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 ) )
(h |^ (a ")) |^ a = h |^ ((a ") * a) by Th24
.= h |^ (1_ G) by GROUP_1:def 5
.= h by Th19 ;
hence ( ( not h in ((Omega). G) |^ a or h in (Omega). G ) & ( not h in (Omega). G or h in ((Omega). G) |^ a ) ) by Th58, STRUCT_0:def 5; :: thesis: verum