let G be Group; :: thesis: (<*> the carrier of G) " = <*> the carrier of G
len (<*> the carrier of G) = 0 ;
then len ((<*> the carrier of G) " ) = 0 by Def4;
hence (<*> the carrier of G) " = <*> the carrier of G ; :: thesis: verum