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₁[ 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₁[z,w]

proof

let z be Element of (product <*H,K*>); :: thesis: ex w being Element of the carrier of (product F) st S₁[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₁[z,w] by A4, A5; :: thesis: verum

end;

consider G being Function of (product <*H,K*>),(product F) such that
A6: for x being Element of (product <*H,K*>) holds S₁[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) )

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
.= h by FINSEQ_1:44, A8 ;
k1 = <*h1,k1*> . 2
.= 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;

then reconsider G = G as Homomorphism of (product <*H,K*>),(product F) by Th23, A1;
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