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,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds

f is Homomorphism of G,(product F)

let q be set ; :: thesis: for F being Group-like associative multMagma-Family of {q}

for f being Function of G,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds

f is Homomorphism of G,(product F)

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

f is Homomorphism of G,(product F)

let f be Function of G,(product F); :: thesis: ( F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) implies f is Homomorphism of G,(product F) )

assume A1: F = q .--> G ; :: thesis: ( ex x being Element of G st not f . x = q .--> x or f is Homomorphism of G,(product F) )

assume A2: for x being Element of G holds f . x = q .--> x ; :: thesis: f is Homomorphism of G,(product F)

A3: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;

for F being Group-like associative multMagma-Family of {q}

for f being Function of G,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds

f is Homomorphism of G,(product F)

let q be set ; :: thesis: for F being Group-like associative multMagma-Family of {q}

for f being Function of G,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds

f is Homomorphism of G,(product F)

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

f is Homomorphism of G,(product F)

let f be Function of G,(product F); :: thesis: ( F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) implies f is Homomorphism of G,(product F) )

assume A1: F = q .--> G ; :: thesis: ( ex x being Element of G st not f . x = q .--> x or f is Homomorphism of G,(product F) )

assume A2: for x being Element of G holds f . x = q .--> x ; :: thesis: f is Homomorphism of G,(product F)

A3: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;

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

hence
f is Homomorphism of G,(product F)
by GROUP_6:def 6; :: thesis: verumlet 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 (product F) ;

set ga = q .--> a;

set gb = q .--> b;

consider gab being Function such that

A6: ( fa * fb = gab & dom gab = dom (Carrier F) & ( for y being object st y in dom (Carrier F) holds

gab . y in (Carrier F) . y ) ) by CARD_3:def 5, A3;

A7: for z being object st z in dom gab holds

gab . z = a * b

.= q .--> (a * b) by A6, PARTFUN1:def 2

.= f . (a * b) by A2 ;

hence f . (a * b) = (f . a) * (f . b) by A6; :: thesis: verum

end;A4: f . a = q .--> a by A2;

A5: f . b = q .--> b by A2;

reconsider fa = f . a, fb = f . b as Element of (product F) ;

set ga = q .--> a;

set gb = q .--> b;

consider gab being Function such that

A6: ( fa * fb = gab & dom gab = dom (Carrier F) & ( for y being object st y in dom (Carrier F) holds

gab . y in (Carrier F) . y ) ) by CARD_3:def 5, A3;

A7: for z being object st z in dom gab holds

gab . z = a * b

proof

gab =
(dom gab) --> (a * b)
by A7, FUNCOP_1:11
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 A1, FUNCOP_1:7, A8, A6;

A10: (q .--> a) . z = a by FUNCOP_1:7, A8, A6;

(q .--> b) . z = b by FUNCOP_1:7, A8, A6;

hence gab . z = a * b by A4, A5, A6, A8, A9, A10, GROUP_7:1; :: thesis: verum

end;assume A8: z in dom gab ; :: thesis: gab . z = a * b

A9: G = F . z by A1, FUNCOP_1:7, A8, A6;

A10: (q .--> a) . z = a by FUNCOP_1:7, A8, A6;

(q .--> b) . z = b by FUNCOP_1:7, A8, A6;

hence gab . z = a * b by A4, A5, A6, A8, A9, A10, GROUP_7:1; :: thesis: verum

.= q .--> (a * b) by A6, PARTFUN1:def 2

.= f . (a * b) by A2 ;

hence f . (a * b) = (f . a) * (f . b) by A6; :: thesis: verum