Abstract: A formal axiom system for the algebraic manipulation of regular expressions will be discussed. This system is consistent and complete; equations derivable within this system are precisely the ones that are true. The completeness proof is based on the uniqueness of solution of certain equations of regular expressions.