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*>),() 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*>),() 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*>),() 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*>),() 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*>),() 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*>),() 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*>),() 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 S1[ 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 () st S1[z,w]
proof
let z be Element of (product <*H,K*>); :: thesis: ex w being Element of the carrier of () st S1[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 ;
set w = g +* (q .--> k);
g +* (q .--> k) in the carrier of () by A1, A5, Th22;
hence ex w being Element of the carrier of () st S1[z,w] by A4, A5; :: thesis: verum
end;
consider G being Function of (product <*H,K*>),() such that
A6: for x being Element of (product <*H,K*>) holds S1[x,G . x] from 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
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 ;
k1 = <*h1,k1*> . 2 by FINSEQ_1:44
.= k by ;
hence ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) by A8, A9; :: thesis: verum
end;
then reconsider G = G as Homomorphism of (product <*H,K*>),() by ;
G is bijective by Th24, A1, A7;
hence ex G being Homomorphism of (product <*H,K*>),() 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