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 bijective

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 bijective

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 bijective

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 bijective

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 bijective

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 bijective )

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 bijective

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 bijective )

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 bijective

set HK = <*H,K*>;

A3: dom (Carrier F0) = I0 by PARTFUN1:def 2;

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

A5: dom F0 = I0 by PARTFUN1:def 2;

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

for x1, x2 being object st x1 in the carrier of (product <*H,K*>) & x2 in the carrier of (product <*H,K*>) & G . x1 = G . x2 holds

x1 = x2

for y being object st y in the carrier of (product F) holds

ex x being object st

( x in the carrier of (product <*H,K*>) & y = G . x )

then G is onto by FUNCT_2:def 3;

hence G is bijective by A33; :: thesis: verum

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 bijective

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 bijective

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 bijective

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 bijective

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 bijective

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 bijective )

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 bijective

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 bijective )

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 bijective

set HK = <*H,K*>;

A3: dom (Carrier F0) = I0 by PARTFUN1:def 2;

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

A5: dom F0 = I0 by PARTFUN1:def 2;

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

for x1, x2 being object st x1 in the carrier of (product <*H,K*>) & x2 in the carrier of (product <*H,K*>) & G . x1 = G . x2 holds

x1 = x2

proof

then A33:
G is one-to-one
by FUNCT_2:19;
let z1, z2 be object ; :: thesis: ( z1 in the carrier of (product <*H,K*>) & z2 in the carrier of (product <*H,K*>) & G . z1 = G . z2 implies z1 = z2 )

assume A8: ( z1 in the carrier of (product <*H,K*>) & z2 in the carrier of (product <*H,K*>) & G . z1 = G . z2 ) ; :: thesis: z1 = z2

then reconsider x1 = z1, x2 = z2 as Element of (product <*H,K*>) ;

consider h1 being Element of H, k1 being Element of K such that

A9: x1 = <*h1,k1*> by TOPALG_4:1;

consider h2 being Element of H, k2 being Element of K such that

A10: x2 = <*h2,k2*> by TOPALG_4:1;

consider g1 being Function such that

A11: ( g1 = G0 . h1 & G . <*h1,k1*> = g1 +* (q .--> k1) ) by A2;

consider g2 being Function such that

A12: ( g2 = G0 . h2 & G . <*h2,k2*> = g2 +* (q .--> k2) ) by A2;

reconsider g1 = g1 as I0 -defined total Function by Lm6, A11;

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

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

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

A15: for i being set st i in I0 holds

( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i )

for x being object st x in dom g1 holds

g1 . x = g2 . x

( ga . q = k1 & gb . q = k2 )

end;assume A8: ( z1 in the carrier of (product <*H,K*>) & z2 in the carrier of (product <*H,K*>) & G . z1 = G . z2 ) ; :: thesis: z1 = z2

then reconsider x1 = z1, x2 = z2 as Element of (product <*H,K*>) ;

consider h1 being Element of H, k1 being Element of K such that

A9: x1 = <*h1,k1*> by TOPALG_4:1;

consider h2 being Element of H, k2 being Element of K such that

A10: x2 = <*h2,k2*> by TOPALG_4:1;

consider g1 being Function such that

A11: ( g1 = G0 . h1 & G . <*h1,k1*> = g1 +* (q .--> k1) ) by A2;

consider g2 being Function such that

A12: ( g2 = G0 . h2 & G . <*h2,k2*> = g2 +* (q .--> k2) ) by A2;

reconsider g1 = g1 as I0 -defined total Function by Lm6, A11;

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

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

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

A15: for i being set st i in I0 holds

( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i )

proof

A24:
dom g2 = I0
by PARTFUN1:def 2;
let i be set ; :: thesis: ( i in I0 implies ( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i ) )

assume A16: i in I0 ; :: thesis: ( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i )

A17: dom g1 = I0 by PARTFUN1:def 2;

A18: dom g2 = I0 by PARTFUN1:def 2;

A19: i in (dom g1) \/ (dom (q .--> k1)) by A17, A16, XBOOLE_0:def 3;

A20: i in (dom g2) \/ (dom (q .--> k2)) by A18, A16, XBOOLE_0:def 3;

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

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

hence ( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i ) by A21, A1, A19, A20, FUNCT_4:def 1; :: thesis: verum

end;assume A16: i in I0 ; :: thesis: ( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i )

A17: dom g1 = I0 by PARTFUN1:def 2;

A18: dom g2 = I0 by PARTFUN1:def 2;

A19: i in (dom g1) \/ (dom (q .--> k1)) by A17, A16, XBOOLE_0:def 3;

A20: i in (dom g2) \/ (dom (q .--> k2)) by A18, A16, XBOOLE_0:def 3;

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

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

hence ( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i ) by A21, A1, A19, A20, FUNCT_4:def 1; :: thesis: verum

for x being object st x in dom g1 holds

g1 . x = g2 . x

proof

then A26:
G0 . h1 = G0 . h2
by A11, A12, FUNCT_1:2, PARTFUN1:def 2, A24;
let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )

assume A25: x in dom g1 ; :: thesis: g1 . x = g2 . x

thus g1 . x = ga . x by A15, A25

.= g2 . x by A15, A25, A11, A12, A9, A10, A8 ; :: thesis: verum

end;assume A25: x in dom g1 ; :: thesis: g1 . x = g2 . x

thus g1 . x = ga . x by A15, A25

.= g2 . x by A15, A25, A11, A12, A9, A10, A8 ; :: thesis: verum

( ga . q = k1 & gb . q = k2 )

proof

hence
z1 = z2
by A9, A10, A26, A1, FUNCT_2:19, A11, A12, A8; :: thesis: verum
A27:
q in {q}
by TARSKI:def 1;

A28: q in dom (q .--> k1) by TARSKI:def 1;

A29: q in dom (q .--> k2) by TARSKI:def 1;

A30: q in (dom g1) \/ (dom (q .--> k1)) by A27, XBOOLE_0:def 3;

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

A32: ga . q = (q .--> k1) . q by A28, A30, FUNCT_4:def 1

.= k1 by FUNCOP_1:7, A27 ;

gb . q = (q .--> k2) . q by A29, A31, FUNCT_4:def 1

.= k2 by FUNCOP_1:7, A27 ;

hence ( ga . q = k1 & gb . q = k2 ) by A32; :: thesis: verum

end;A28: q in dom (q .--> k1) by TARSKI:def 1;

A29: q in dom (q .--> k2) by TARSKI:def 1;

A30: q in (dom g1) \/ (dom (q .--> k1)) by A27, XBOOLE_0:def 3;

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

A32: ga . q = (q .--> k1) . q by A28, A30, FUNCT_4:def 1

.= k1 by FUNCOP_1:7, A27 ;

gb . q = (q .--> k2) . q by A29, A31, FUNCT_4:def 1

.= k2 by FUNCOP_1:7, A27 ;

hence ( ga . q = k1 & gb . q = k2 ) by A32; :: thesis: verum

for y being object st y in the carrier of (product F) holds

ex x being object st

( x in the carrier of (product <*H,K*>) & y = G . x )

proof

then
rng G = the carrier of (product F)
by FUNCT_2:10;
let y be object ; :: thesis: ( y in the carrier of (product F) implies ex x being object st

( x in the carrier of (product <*H,K*>) & y = G . x ) )

assume A34: y in the carrier of (product F) ; :: thesis: ex x being object st

( x in the carrier of (product <*H,K*>) & y = G . x )

then reconsider y = y as I -defined total Function by Lm6;

A35: q in {q} by TARSKI:def 1;

A36: q in dom (q .--> K) by TARSKI:def 1;

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

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

.= K by FUNCOP_1:7, A35 ;

ex R being non empty multMagma st

( R = F . q & y . q in the carrier of R ) by Lm7, A34;

then reconsider k = y . q as Element of K by A38;

reconsider y0 = y | I0 as I0 -defined Function ;

A39: the carrier of (product F0) = product (Carrier F0) by GROUP_7:def 2;

I = dom y by PARTFUN1:def 2;

then A40: dom y0 = I0 by RELAT_1:62, A1, XBOOLE_1:7;

for i being object st i in dom (Carrier F0) holds

y0 . i in (Carrier F0) . i

then y0 in rng G0 by A1, FUNCT_2:def 3;

then consider h being Element of H such that

A48: y0 = G0 . h by FUNCT_2:113;

A49: dom y = I by PARTFUN1:def 2;

then y | {q} = q .--> k by FUNCT_7:6;

then A50: y = (y | I0) +* (q .--> k) by A1, A49, FUNCT_4:70;

consider g being Function such that

A51: ( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) by A2;

thus ex x being object st

( x in the carrier of (product <*H,K*>) & y = G . x ) by A48, A50, A51; :: thesis: verum

end;( x in the carrier of (product <*H,K*>) & y = G . x ) )

assume A34: y in the carrier of (product F) ; :: thesis: ex x being object st

( x in the carrier of (product <*H,K*>) & y = G . x )

then reconsider y = y as I -defined total Function by Lm6;

A35: q in {q} by TARSKI:def 1;

A36: q in dom (q .--> K) by TARSKI:def 1;

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

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

.= K by FUNCOP_1:7, A35 ;

ex R being non empty multMagma st

( R = F . q & y . q in the carrier of R ) by Lm7, A34;

then reconsider k = y . q as Element of K by A38;

reconsider y0 = y | I0 as I0 -defined Function ;

A39: the carrier of (product F0) = product (Carrier F0) by GROUP_7:def 2;

I = dom y by PARTFUN1:def 2;

then A40: dom y0 = I0 by RELAT_1:62, A1, XBOOLE_1:7;

for i being object st i in dom (Carrier F0) holds

y0 . i in (Carrier F0) . i

proof

then
y0 in the carrier of (product F0)
by A40, A3, CARD_3:def 5, A39;
let i be object ; :: thesis: ( i in dom (Carrier F0) implies y0 . i in (Carrier F0) . i )

assume A41: i in dom (Carrier F0) ; :: thesis: y0 . i in (Carrier F0) . i

then A42: i in I0 ;

A43: i in (dom F0) \/ (dom (q .--> K)) by A5, A41, XBOOLE_0:def 3;

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

A45: I0 c= I by XBOOLE_1:7, A1;

A46: ex R being 1-sorted st

( R = F0 . i & (Carrier F0) . i = the carrier of R ) by A41, PRALG_1:def 15;

ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by A42, A45, PRALG_1:def 15;

then A47: (Carrier F0) . i = (Carrier F) . i by A43, FUNCT_4:def 1, A1, A44, A46;

ex g being Function st

( y = g & dom g = dom (Carrier F) & ( for i being object st i in dom (Carrier F) holds

g . i in (Carrier F) . i ) ) by CARD_3:def 5, A34, A6;

then y . i in (Carrier F) . i by A45, A4, A42;

hence y0 . i in (Carrier F0) . i by A47, A41, FUNCT_1:49; :: thesis: verum

end;assume A41: i in dom (Carrier F0) ; :: thesis: y0 . i in (Carrier F0) . i

then A42: i in I0 ;

A43: i in (dom F0) \/ (dom (q .--> K)) by A5, A41, XBOOLE_0:def 3;

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

A45: I0 c= I by XBOOLE_1:7, A1;

A46: ex R being 1-sorted st

( R = F0 . i & (Carrier F0) . i = the carrier of R ) by A41, PRALG_1:def 15;

ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by A42, A45, PRALG_1:def 15;

then A47: (Carrier F0) . i = (Carrier F) . i by A43, FUNCT_4:def 1, A1, A44, A46;

ex g being Function st

( y = g & dom g = dom (Carrier F) & ( for i being object st i in dom (Carrier F) holds

g . i in (Carrier F) . i ) ) by CARD_3:def 5, A34, A6;

then y . i in (Carrier F) . i by A45, A4, A42;

hence y0 . i in (Carrier F0) . i by A47, A41, FUNCT_1:49; :: thesis: verum

then y0 in rng G0 by A1, FUNCT_2:def 3;

then consider h being Element of H such that

A48: y0 = G0 . h by FUNCT_2:113;

A49: dom y = I by PARTFUN1:def 2;

then y | {q} = q .--> k by FUNCT_7:6;

then A50: y = (y | I0) +* (q .--> k) by A1, A49, FUNCT_4:70;

consider g being Function such that

A51: ( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) by A2;

thus ex x being object st

( x in the carrier of (product <*H,K*>) & y = G . x ) by A48, A50, A51; :: thesis: verum

then G is onto by FUNCT_2:def 3;

hence G is bijective by A33; :: thesis: verum