let G be Group; :: thesis: (<*> the carrier of G) |^ (<*> INT ) = {}
len (<*> the carrier of G) = 0 ;
then len ((<*> the carrier of G) |^ (<*> INT )) = 0 by Def4;
hence (<*> the carrier of G) |^ (<*> INT ) = {} ; :: thesis: verum