let G be Group; :: thesis: for q being set
for F being Group-like associative multMagma-Family of {q}
for f being Function of G,() st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is Homomorphism of G,()

let q be set ; :: thesis: for F being Group-like associative multMagma-Family of {q}
for f being Function of G,() st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is Homomorphism of G,()

let F be Group-like associative multMagma-Family of {q}; :: thesis: for f being Function of G,() st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is Homomorphism of G,()

let f be Function of G,(); :: thesis: ( F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) implies f is Homomorphism of G,() )
assume A1: F = q .--> G ; :: thesis: ( ex x being Element of G st not f . x = q .--> x or f is Homomorphism of G,() )
assume A2: for x being Element of G holds f . x = q .--> x ; :: thesis: f is Homomorphism of G,()
A3: the carrier of () = product () by GROUP_7:def 2;
now :: thesis: for a, b being Element of G holds f . (a * b) = (f . a) * (f . b)
let a, b be Element of G; :: thesis: f . (a * b) = (f . a) * (f . b)
A4: f . a = q .--> a by A2;
A5: f . b = q .--> b by A2;
reconsider fa = f . a, fb = f . b as Element of () ;
set ga = q .--> a;
set gb = q .--> b;
consider gab being Function such that
A6: ( fa * fb = gab & dom gab = dom () & ( for y being object st y in dom () holds
gab . y in () . y ) ) by ;
A7: for z being object st z in dom gab holds
gab . z = a * b
proof
let z be object ; :: thesis: ( z in dom gab implies gab . z = a * b )
assume A8: z in dom gab ; :: thesis: gab . z = a * b
A9: G = F . z by ;
A10: (q .--> a) . z = a by ;
(q .--> b) . z = b by ;
hence gab . z = a * b by A4, A5, A6, A8, A9, A10, GROUP_7:1; :: thesis: verum
end;
gab = (dom gab) --> (a * b) by
.= q .--> (a * b) by
.= f . (a * b) by A2 ;
hence f . (a * b) = (f . a) * (f . b) by A6; :: thesis: verum
end;
hence f is Homomorphism of G,() by GROUP_6:def 6; :: thesis: verum