let G be Group; :: thesis: for a being Element of G holds ((Omega). G) |^ a = (Omega). G
let a be Element of G; :: thesis: ((Omega). G) |^ a = (Omega). G
let h be Element of G; :: according to GROUP_2:def 6 :: thesis: ( ( not h in ((Omega). G) |^ a or h in (Omega). G ) & ( not h in (Omega). G or h in ((Omega). G) |^ a ) )
A1: h |^ (a " ) in multMagma(# the carrier of G,the multF of G #) by STRUCT_0:def 5;
(h |^ (a " )) |^ a = h |^ ((a " ) * a) by Th29
.= h |^ (1_ G) by GROUP_1:def 6
.= h by Th24 ;
hence ( ( not h in ((Omega). G) |^ a or h in (Omega). G ) & ( not h in (Omega). G or h in ((Omega). G) |^ a ) ) by A1, Th70, STRUCT_0:def 5; :: thesis: verum