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 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*>),() 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*>),() 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*>),() 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*>),() 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*>),() 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*>),() 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*>),(); :: 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 () = I by PARTFUN1:def 2;
A5: dom F0 = I0 by PARTFUN1:def 2;
A6: the carrier of () = product () 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
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 ;
reconsider g2 = g2 as I0 -defined total Function by ;
reconsider ga = g1 +* (q .--> k1) as I -defined total Function by ;
reconsider gb = g2 +* (q .--> k2) as I -defined total Function by ;
A15: for i being set st i in I0 holds
( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i )
proof
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 ;
A20: i in (dom g2) \/ (dom (q .--> k2)) by ;
A21: i in (dom F0) \/ (dom (q .--> K)) by ;
not i in dom (q .--> K) by ;
hence ( ga . i = g1 . i & gb . i = g2 . i & F . i = F0 . i ) by ; :: thesis: verum
end;
A24: dom g2 = I0 by PARTFUN1:def 2;
for x being object st x in dom g1 holds
g1 . x = g2 . x
proof
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
.= g2 . x by A15, A25, A11, A12, A9, A10, A8 ; :: thesis: verum
end;
then A26: G0 . h1 = G0 . h2 by ;
( ga . q = k1 & gb . q = k2 )
proof
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 ;
A31: q in (dom g2) \/ (dom (q .--> k2)) by ;
A32: ga . q = (q .--> k1) . q by
.= k1 by ;
gb . q = (q .--> k2) . q by
.= k2 by ;
hence ( ga . q = k1 & gb . q = k2 ) by A32; :: thesis: verum
end;
hence z1 = z2 by A9, A10, A26, A1, FUNCT_2:19, A11, A12, A8; :: thesis: verum
end;
then A33: G is one-to-one by FUNCT_2:19;
for y being object st y in the carrier of () holds
ex x being object st
( x in the carrier of (product <*H,K*>) & y = G . x )
proof
let y be object ; :: thesis: ( y in the carrier of () implies ex x being object st
( x in the carrier of (product <*H,K*>) & y = G . x ) )

assume A34: y in the carrier of () ; :: 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 ;
A38: F . q = (q .--> K) . q by
.= K by ;
ex R being non empty multMagma st
( R = F . q & y . q in the carrier of R ) by ;
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 ;
for i being object st i in dom (Carrier F0) holds
y0 . i in (Carrier F0) . i
proof
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 ;
A44: not i in dom (q .--> K) by ;
A45: I0 c= I by ;
A46: ex R being 1-sorted st
( R = F0 . i & (Carrier F0) . i = the carrier of R ) by ;
ex R being 1-sorted st
( R = F . i & () . i = the carrier of R ) by ;
then A47: (Carrier F0) . i = () . i by ;
ex g being Function st
( y = g & dom g = dom () & ( for i being object st i in dom () holds
g . i in () . i ) ) by ;
then y . i in () . i by A45, A4, A42;
hence y0 . i in (Carrier F0) . i by ; :: thesis: verum
end;
then y0 in the carrier of (product F0) by ;
then y0 in rng G0 by ;
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 ;
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 ; :: thesis: verum
end;
then rng G = the carrier of () by FUNCT_2:10;
then G is onto by FUNCT_2:def 3;
hence G is bijective by A33; :: thesis: verum