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 (product F0),H 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 x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,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 (product F0),H 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 x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,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 (product F0),H 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 x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*> ) )

let H, K be Group; :: thesis: for q being Element of I
for G0 being Homomorphism of (product F0),H 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 x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*> ) )

let q be Element of I; :: thesis: for G0 being Homomorphism of (product F0),H 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 x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*> ) )

let G0 be Homomorphism of (product F0),H; :: 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 x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,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 x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*> ) )

set L0 = G0 " ;
A2: rng G0 = the carrier of H by ;
then reconsider L0 = G0 " as Function of H,(product F0) by ;
A3: ( L0 * G0 = id the carrier of (product F0) & G0 * L0 = id the carrier of H ) by ;
A4: L0 is onto by ;
reconsider L0 = L0 as Homomorphism of H,(product F0) by ;
consider L being Homomorphism of (product <*H,K*>),() such that
A5: ( L is bijective & ( for h being Element of H
for k being Element of K ex g being Function st
( g = L0 . h & L . <*h,k*> = g +* (q .--> k) ) ) ) by Th27, A1, A4;
set G = L " ;
A6: rng L = the carrier of () by ;
then reconsider G = L " as Function of (),(product <*H,K*>) by ;
A7: ( G * L = id the carrier of (product <*H,K*>) & L * G = id the carrier of () ) by ;
A8: G is onto by ;
reconsider G = G as Homomorphism of (),(product <*H,K*>) by ;
for x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*>
proof
let x0 be Function; :: thesis: for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*>

let k be Element of K; :: thesis: for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*>

let h be Element of H; :: thesis: ( h = G0 . x0 & x0 in product F0 implies G . (x0 +* (q .--> k)) = <*h,k*> )
assume A9: ( h = G0 . x0 & x0 in product F0 ) ; :: thesis: G . (x0 +* (q .--> k)) = <*h,k*>
consider g being Function such that
A10: ( g = L0 . h & L . <*h,k*> = g +* (q .--> k) ) by A5;
g = x0 by ;
hence G . (x0 +* (q .--> k)) = <*h,k*> by ; :: thesis: verum
end;
hence ex G being Homomorphism of (),(product <*H,K*>) st
( G is bijective & ( for x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*> ) ) by A8, A5; :: thesis: verum