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 F),(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 F),(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 F),(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 F),(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 F),(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 F),(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 F),(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 FUNCT_2:def 3, A1;
then reconsider L0 = G0 " as Function of H,(product F0) by FUNCT_2:25, A1;
A3: ( L0 * G0 = id the carrier of (product F0) & G0 * L0 = id the carrier of H ) by A1, A2, FUNCT_2:29;
A4: L0 is onto by A3, FUNCT_2:23;
reconsider L0 = L0 as Homomorphism of H,(product F0) by A1, GROUP_6:62;
consider L being Homomorphism of (product <*H,K*>),(product F) 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 (product F) by FUNCT_2:def 3, A5;
then reconsider G = L " as Function of (product F),(product <*H,K*>) by FUNCT_2:25, A5;
A7: ( G * L = id the carrier of (product <*H,K*>) & L * G = id the carrier of (product F) ) by A5, A6, FUNCT_2:29;
A8: G is onto by A7, FUNCT_2:23;
reconsider G = G as Homomorphism of (product F),(product <*H,K*>) by A5, GROUP_6:62;
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 A10, A1, A9, FUNCT_2:26;
hence G . (x0 +* (q .--> k)) = <*h,k*> by A5, FUNCT_2:26, A10; :: thesis: verum

end;

hence ex G being Homomorphism of (product F),(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