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 Homomorphism of H,(product F0) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

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 Homomorphism of H,(product F0) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

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 Homomorphism of H,(product F0) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

let H, K be Group; :: thesis: for q being Element of I

for G0 being Homomorphism of H,(product F0) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

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

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

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

( G is bijective & ( 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) ) ) ) )

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

( G is bijective & ( 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) ) ) )

set HK = <*H,K*>;

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

defpred S_{1}[ set , set ] means ex h being Element of H ex k being Element of K ex g being Function st

( $1 = <*h,k*> & g = G0 . h & $2 = g +* (q .--> k) );

A3: for z being Element of (product <*H,K*>) ex w being Element of the carrier of (product F) st S_{1}[z,w]

A6: for x being Element of (product <*H,K*>) holds S_{1}[x,G . x]
from FUNCT_2:sch 3(A3);

A7: 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) )

G is bijective by Th24, A1, A7;

hence ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) ) by A7; :: 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 Homomorphism of H,(product F0) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

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 Homomorphism of H,(product F0) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

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 Homomorphism of H,(product F0) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

let H, K be Group; :: thesis: for q being Element of I

for G0 being Homomorphism of H,(product F0) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

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

ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) )

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

( G is bijective & ( 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) ) ) ) )

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

( G is bijective & ( 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) ) ) )

set HK = <*H,K*>;

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

defpred S

( $1 = <*h,k*> & g = G0 . h & $2 = g +* (q .--> k) );

A3: for z being Element of (product <*H,K*>) ex w being Element of the carrier of (product F) st S

proof

consider G being Function of (product <*H,K*>),(product F) such that
let z be Element of (product <*H,K*>); :: thesis: ex w being Element of the carrier of (product F) st S_{1}[z,w]

consider h being Element of H, k being Element of K such that

A4: z = <*h,k*> by TOPALG_4:1;

consider g being Function such that

A5: ( G0 . h = g & dom g = dom (Carrier F0) & ( for y being object st y in dom (Carrier F0) holds

g . y in (Carrier F0) . y ) ) by CARD_3:def 5, A2;

set w = g +* (q .--> k);

g +* (q .--> k) in the carrier of (product F) by A1, A5, Th22;

hence ex w being Element of the carrier of (product F) st S_{1}[z,w]
by A4, A5; :: thesis: verum

end;consider h being Element of H, k being Element of K such that

A4: z = <*h,k*> by TOPALG_4:1;

consider g being Function such that

A5: ( G0 . h = g & dom g = dom (Carrier F0) & ( for y being object st y in dom (Carrier F0) holds

g . y in (Carrier F0) . y ) ) by CARD_3:def 5, A2;

set w = g +* (q .--> k);

g +* (q .--> k) in the carrier of (product F) by A1, A5, Th22;

hence ex w being Element of the carrier of (product F) st S

A6: for x being Element of (product <*H,K*>) holds S

A7: 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) )

proof

then reconsider G = G as Homomorphism of (product <*H,K*>),(product F) by Th23, A1;
let h be Element of H; :: thesis: for k being Element of K ex g being Function st

( g = G0 . h & G . <*h,k*> = g +* (q .--> k) )

let k be Element of K; :: thesis: ex g being Function st

( g = G0 . h & G . <*h,k*> = g +* (q .--> k) )

reconsider z = <*h,k*> as Element of (product <*H,K*>) ;

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

A8: ( z = <*h1,k1*> & g = G0 . h1 & G . z = g +* (q .--> k1) ) by A6;

A9: h1 = <*h1,k1*> . 1 by FINSEQ_1:44

.= h by FINSEQ_1:44, A8 ;

k1 = <*h1,k1*> . 2 by FINSEQ_1:44

.= k by FINSEQ_1:44, A8 ;

hence ex g being Function st

( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) by A8, A9; :: thesis: verum

end;( g = G0 . h & G . <*h,k*> = g +* (q .--> k) )

let k be Element of K; :: thesis: ex g being Function st

( g = G0 . h & G . <*h,k*> = g +* (q .--> k) )

reconsider z = <*h,k*> as Element of (product <*H,K*>) ;

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

A8: ( z = <*h1,k1*> & g = G0 . h1 & G . z = g +* (q .--> k1) ) by A6;

A9: h1 = <*h1,k1*> . 1 by FINSEQ_1:44

.= h by FINSEQ_1:44, A8 ;

k1 = <*h1,k1*> . 2 by FINSEQ_1:44

.= k by FINSEQ_1:44, A8 ;

hence ex g being Function st

( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) by A8, A9; :: thesis: verum

G is bijective by Th24, A1, A7;

hence ex G being Homomorphism of (product <*H,K*>),(product F) st

( G is bijective & ( 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) ) ) ) by A7; :: thesis: verum