now

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

now

let g1, g2 be Element of G; :: thesis: f . (g1 * g2) = (f . g1) * (f . g2)
reconsider g1' = g1, g2' = g2 as Element of G' by A2;
f . (g1 * g2) = f' . (g1' * g2') by A2
.= (f' . g1') * (f' . g2') by GROUP_6:def 7
.= 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 7; :: 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:47; :: thesis: verum