let G be Group; :: thesis: for a being Element of G holds (<*> the carrier of G) |^ a = {}
let a be Element of G; :: thesis: (<*> the carrier of G) |^ a = {}
len ((<*> the carrier of G) |^ a) = len (<*> the carrier of G) by Def1
.= 0 ;
hence (<*> the carrier of G) |^ a = {} ; :: thesis: verum