((<*u*> ^ q) . 1) \+\ u = {} ;
then u = (<*u*> ^ q) . 1 by Th29
.= (U -firstChar) . (<*u*> ^ q) by Th6 ;
hence ((U -firstChar) . (<*u*> ^ q)) \+\ u is empty ; :: thesis: verum