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 5
.= 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