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