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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F) )

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*>),(product F) 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*>),(product F)

let G be Function of (product <*H,K*>),(product F); :: 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*>),(product F) )

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*>),(product F)

set HK = <*H,K*>;

A3: dom (Carrier F) = I by PARTFUN1:def 2;

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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F)

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*>),(product F) 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*>),(product F) )

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*>),(product F) 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*>),(product F)

let G be Function of (product <*H,K*>),(product F); :: 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*>),(product F) )

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*>),(product F)

set HK = <*H,K*>;

A3: dom (Carrier F) = I by PARTFUN1:def 2;

now :: thesis: for a, b being Element of (product <*H,K*>) holds G . (a * b) = (G . a) * (G . b)

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

reconsider g2 = g2 as I0 -defined total Function by A7, Lm6;

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 (product F) ;

reconsider ga = g1 +* (q .--> k1) as I -defined total Function by Lm6, A6;

reconsider gb = g2 +* (q .--> k2) as I -defined total Function by Lm6, A7;

reconsider pab = Ga * Gb as I -defined total Function by Lm6;

A13: dom pab = dom (Carrier F) by PARTFUN1:def 2, A3;

A14: g12 = (G0 . h1) * (G0 . h2) by A1, GROUP_6:def 6;

reconsider gab = G . (a * b) as I -defined total Function by Lm6;

A15: gab = g12 +* (q .--> (k1 * k2)) by A4, A5, GROUP_7:29, A12;

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 )

pab . x = gab . x

gab . x = pab . x

end;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 A6, Lm6;

reconsider g2 = g2 as I0 -defined total Function by A7, Lm6;

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 (product F) ;

reconsider ga = g1 +* (q .--> k1) as I -defined total Function by Lm6, A6;

reconsider gb = g2 +* (q .--> k2) as I -defined total Function by Lm6, A7;

reconsider pab = Ga * Gb as I -defined total Function by Lm6;

A13: dom pab = dom (Carrier F) by PARTFUN1:def 2, A3;

A14: g12 = (G0 . h1) * (G0 . h2) by A1, GROUP_6:def 6;

reconsider gab = G . (a * b) as I -defined total Function by Lm6;

A15: gab = g12 +* (q .--> (k1 * k2)) by A4, A5, GROUP_7:29, A12;

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

A29:
( ga . q = k1 & gb . q = k2 & gab . q = k1 * k2 & F . q = K )
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 A18, A17, XBOOLE_0:def 3;

A23: i in (dom g2) \/ (dom (q .--> k2)) by A19, A17, XBOOLE_0:def 3;

A24: i in (dom g12) \/ (dom (q .--> (k1 * k2))) by A20, A17, XBOOLE_0:def 3;

A25: i in (dom F0) \/ (dom (q .--> K)) by A21, A17, XBOOLE_0:def 3;

not i in dom (q .--> K) by A1, A17, FUNCOP_1:75;

hence ( ga . i = g1 . i & gb . i = g2 . i & gab . i = g12 . i & F . i = F0 . i ) by A25, FUNCT_4:def 1, A1, A22, A23, A24, A15; :: thesis: verum

end;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 A18, A17, XBOOLE_0:def 3;

A23: i in (dom g2) \/ (dom (q .--> k2)) by A19, A17, XBOOLE_0:def 3;

A24: i in (dom g12) \/ (dom (q .--> (k1 * k2))) by A20, A17, XBOOLE_0:def 3;

A25: i in (dom F0) \/ (dom (q .--> K)) by A21, A17, XBOOLE_0:def 3;

not i in dom (q .--> K) by A1, A17, FUNCOP_1:75;

hence ( ga . i = g1 . i & gb . i = g2 . i & gab . i = g12 . i & F . i = F0 . i ) by A25, FUNCT_4:def 1, A1, A22, A23, A24, A15; :: thesis: verum

proof

A42:
for x being set st x in I0 holds
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 A30, XBOOLE_0:def 3;

A36: q in (dom g2) \/ (dom (q .--> k2)) by A30, XBOOLE_0:def 3;

A37: q in (dom g12) \/ (dom (q .--> (k1 * k2))) by A30, XBOOLE_0:def 3;

A38: q in (dom F0) \/ (dom (q .--> K)) by A30, XBOOLE_0:def 3;

A39: ga . q = (q .--> k1) . q by A31, A35, FUNCT_4:def 1

.= k1 by FUNCOP_1:7, A30 ;

A40: gb . q = (q .--> k2) . q by A32, A36, FUNCT_4:def 1

.= k2 by FUNCOP_1:7, A30 ;

A41: gab . q = (q .--> (k1 * k2)) . q by A33, A37, A15, FUNCT_4:def 1

.= k1 * k2 by FUNCOP_1:7, A30 ;

F . q = (q .--> K) . q by A34, A38, A1, FUNCT_4:def 1

.= K by FUNCOP_1:7, A30 ;

hence ( ga . q = k1 & gb . q = k2 & gab . q = k1 * k2 & F . q = K ) by A39, A40, A41; :: thesis: verum

end;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 A30, XBOOLE_0:def 3;

A36: q in (dom g2) \/ (dom (q .--> k2)) by A30, XBOOLE_0:def 3;

A37: q in (dom g12) \/ (dom (q .--> (k1 * k2))) by A30, XBOOLE_0:def 3;

A38: q in (dom F0) \/ (dom (q .--> K)) by A30, XBOOLE_0:def 3;

A39: ga . q = (q .--> k1) . q by A31, A35, FUNCT_4:def 1

.= k1 by FUNCOP_1:7, A30 ;

A40: gb . q = (q .--> k2) . q by A32, A36, FUNCT_4:def 1

.= k2 by FUNCOP_1:7, A30 ;

A41: gab . q = (q .--> (k1 * k2)) . q by A33, A37, A15, FUNCT_4:def 1

.= k1 * k2 by FUNCOP_1:7, A30 ;

F . q = (q .--> K) . q by A34, A38, A1, FUNCT_4:def 1

.= K by FUNCOP_1:7, A30 ;

hence ( ga . q = k1 & gb . q = k2 & gab . q = k1 * k2 & F . q = K ) by A39, A40, A41; :: thesis: verum

pab . x = gab . x

proof

for x being object st x in dom gab holds
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 A1, XBOOLE_0:def 3;

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 A45, A16, A43;

( x0 = ga . x & y0 = gb . x ) by A16, A43;

hence pab . x = x0 * y0 by A44, A46, GROUP_7:1, A6, A4, A7, A5

.= g12 . x by A14, A6, A7, GROUP_7:1, A43, A45

.= gab . x by A16, A43 ;

:: thesis: verum

end;assume A43: x in I0 ; :: thesis: pab . x = gab . x

then A44: x in I by A1, XBOOLE_0:def 3;

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 A45, A16, A43;

( x0 = ga . x & y0 = gb . x ) by A16, A43;

hence pab . x = x0 * y0 by A44, A46, GROUP_7:1, A6, A4, A7, A5

.= g12 . x by A14, A6, A7, GROUP_7:1, A43, A45

.= gab . x by A16, A43 ;

:: thesis: verum

gab . x = pab . x

proof

hence
G . (a * b) = (G . a) * (G . b)
by A13, PARTFUN1:def 2, A3, FUNCT_1:2; :: thesis: verum
let x be object ; :: thesis: ( x in dom gab implies gab . x = pab . x )

assume x in dom gab ; :: thesis: gab . x = pab . x

end;assume x in dom gab ; :: thesis: gab . x = pab . x