let G be addGroup; :: 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_1A:def 16 :: thesis: ( h in ((Omega). G) * a iff h in (Omega). G )
(h * (- a)) * a = h * ((- a) + a) by Th24
.= h * (0_ G) by Def5
.= h by Th19 ;
hence ( h in ((Omega). G) * a iff h in (Omega). G ) by Th58, STRUCT_0:def 5; :: thesis: verum