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

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 bassume 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;

end;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)

hence
the action of G . o is Homomorphism of G,G
by GROUP_6:def 6; :: thesis: verumlet 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;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