now :: thesis: ( o in O implies the action of G . o is Homomorphism of G,G )

assume A1: o in O ; :: thesis: the action of G . o is Homomorphism of G,G
consider G9 being Group such that
A2: multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of G, the multF of G #) ;
reconsider a = the action of G as Action of O, the carrier of G9 by A2;
a is distributive by A2, Def5;
then reconsider f9 = a . o as Homomorphism of G9,G9 by A1;
reconsider f = f9 as Function of G,G by A2;

now :: thesis: for g1, g2 being Element of G holds f . (g1 * g2) = (f . g1) * (f . g2)

let g1, g2 be Element of G; :: thesis: f . (g1 * g2) = (f . g1) * (f . g2)
reconsider g19 = g1, g29 = g2 as Element of G9 by A2;
f . (g1 * g2) = f9 . (g19 * g29) by A2
.= (f9 . g19) * (f9 . g29) by GROUP_6:def 6
.= the multF of G . ((f . g1),(f . g2)) by A2 ;
hence f . (g1 * g2) = (f . g1) * (f . g2) ; :: thesis: verum

end;

hence the action of G . o is Homomorphism of G,G by GROUP_6:def 6; :: thesis: verum

end;

hence ( ( o in O implies the action of G . o is Homomorphism of G,G ) & ( not o in O implies id the carrier of G is Homomorphism of G,G ) & ( for b₁ being Homomorphism of G,G holds verum ) ) by GROUP_6:38; :: thesis: verum