let I0, I be non empty finite set ; :: thesis: for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),() st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),()

let F0 be Group-like associative multMagma-Family of I0; :: thesis: for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),() st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),()

let F be Group-like associative multMagma-Family of I; :: thesis: for H, K being Group
for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),() st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),()

let H, K be Group; :: thesis: for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),() st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),()

let q be Element of I; :: thesis: for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),() st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),()

let G0 be Function of H,(product F0); :: thesis: ( G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) implies for G being Function of (product <*H,K*>),() st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),() )

assume A1: ( G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) ) ; :: thesis: for G being Function of (product <*H,K*>),() st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),()

let G be Function of (product <*H,K*>),(); :: thesis: ( ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) implies G is Homomorphism of (product <*H,K*>),() )

assume A2: for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ; :: thesis: G is Homomorphism of (product <*H,K*>),()
set HK = <*H,K*>;
A3: dom () = I by PARTFUN1:def 2;
now :: thesis: for a, b being Element of (product <*H,K*>) holds G . (a * b) = (G . a) * (G . b)
let a, b be Element of (product <*H,K*>); :: thesis: G . (a * b) = (G . a) * (G . b)
consider h1 being Element of H, k1 being Element of K such that
A4: a = <*h1,k1*> by TOPALG_4:1;
consider h2 being Element of H, k2 being Element of K such that
A5: b = <*h2,k2*> by TOPALG_4:1;
consider g1 being Function such that
A6: ( g1 = G0 . h1 & G . <*h1,k1*> = g1 +* (q .--> k1) ) by A2;
consider g2 being Function such that
A7: ( g2 = G0 . h2 & G . <*h2,k2*> = g2 +* (q .--> k2) ) by A2;
reconsider g1 = g1 as I0 -defined total Function by ;
reconsider g2 = g2 as I0 -defined total Function by ;
reconsider g12 = G0 . (h1 * h2) as I0 -defined total Function by Lm6;
A12: ex g12 being Function st
( g12 = G0 . (h1 * h2) & G . <*(h1 * h2),(k1 * k2)*> = g12 +* (q .--> (k1 * k2)) ) by A2;
reconsider Ga = G . a, Gb = G . b as Element of () ;
reconsider ga = g1 +* (q .--> k1) as I -defined total Function by ;
reconsider gb = g2 +* (q .--> k2) as I -defined total Function by ;
reconsider pab = Ga * Gb as I -defined total Function by Lm6;
A13: dom pab = dom () by ;
A14: g12 = (G0 . h1) * (G0 . h2) by ;
reconsider gab = G . (a * b) as I -defined total Function by Lm6;
A15: gab = g12 +* (q .--> (k1 * k2)) by ;
A16: for i being set st i in I0 holds
( ga . i = g1 . i & gb . i = g2 . i & gab . i = g12 . i & F . i = F0 . i )
proof
let i be set ; :: thesis: ( i in I0 implies ( ga . i = g1 . i & gb . i = g2 . i & gab . i = g12 . i & F . i = F0 . i ) )
assume A17: i in I0 ; :: thesis: ( ga . i = g1 . i & gb . i = g2 . i & gab . i = g12 . i & F . i = F0 . i )
A18: dom g1 = I0 by PARTFUN1:def 2;
A19: dom g2 = I0 by PARTFUN1:def 2;
A20: dom g12 = I0 by PARTFUN1:def 2;
A21: dom F0 = I0 by PARTFUN1:def 2;
A22: i in (dom g1) \/ (dom (q .--> k1)) by ;
A23: i in (dom g2) \/ (dom (q .--> k2)) by ;
A24: i in (dom g12) \/ (dom (q .--> (k1 * k2))) by ;
A25: i in (dom F0) \/ (dom (q .--> K)) by ;
not i in dom (q .--> K) by ;
hence ( ga . i = g1 . i & gb . i = g2 . i & gab . i = g12 . i & F . i = F0 . i ) by ; :: thesis: verum
end;
A29: ( ga . q = k1 & gb . q = k2 & gab . q = k1 * k2 & F . q = K )
proof
A30: q in {q} by TARSKI:def 1;
A31: q in dom (q .--> k1) by TARSKI:def 1;
A32: q in dom (q .--> k2) by TARSKI:def 1;
A33: q in dom (q .--> (k1 * k2)) by TARSKI:def 1;
A34: q in dom (q .--> K) by TARSKI:def 1;
A35: q in (dom g1) \/ (dom (q .--> k1)) by ;
A36: q in (dom g2) \/ (dom (q .--> k2)) by ;
A37: q in (dom g12) \/ (dom (q .--> (k1 * k2))) by ;
A38: q in (dom F0) \/ (dom (q .--> K)) by ;
A39: ga . q = (q .--> k1) . q by
.= k1 by ;
A40: gb . q = (q .--> k2) . q by
.= k2 by ;
A41: gab . q = (q .--> (k1 * k2)) . q by
.= k1 * k2 by ;
F . q = (q .--> K) . q by
.= K by ;
hence ( ga . q = k1 & gb . q = k2 & gab . q = k1 * k2 & F . q = K ) by ; :: thesis: verum
end;
A42: for x being set st x in I0 holds
pab . x = gab . x
proof
let x be set ; :: thesis: ( x in I0 implies pab . x = gab . x )
assume A43: x in I0 ; :: thesis: pab . x = gab . x
then A44: x in I by ;
consider S being non empty multMagma such that
A45: ( S = F0 . x & g1 . x in the carrier of S ) by A43, Lm7, A6;
reconsider x0 = g1 . x as Element of S by A45;
ex R being non empty multMagma st
( R = F0 . x & g2 . x in the carrier of R ) by Lm7, A43, A7;
then reconsider y0 = g2 . x as Element of S by A45;
A46: S = F . x by ;
( x0 = ga . x & y0 = gb . x ) by ;
hence pab . x = x0 * y0 by A44, A46, GROUP_7:1, A6, A4, A7, A5
.= g12 . x by
.= gab . x by ;
:: thesis: verum
end;
for x being object st x in dom gab holds
gab . x = pab . x
proof
let x be object ; :: thesis: ( x in dom gab implies gab . x = pab . x )
assume x in dom gab ; :: thesis: gab . x = pab . x
per cases then ( x in I0 or x in {q} ) by ;
suppose x in I0 ; :: thesis: gab . x = pab . x
hence gab . x = pab . x by A42; :: thesis: verum
end;
suppose x in {q} ; :: thesis: gab . x = pab . x
then x = q by TARSKI:def 1;
hence gab . x = pab . x by A29, GROUP_7:1, A6, A4, A7, A5; :: thesis: verum
end;
end;
end;
hence G . (a * b) = (G . a) * (G . b) by ; :: thesis: verum
end;
hence G is Homomorphism of (product <*H,K*>),() by GROUP_6:def 6; :: thesis: verum