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*>

( 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

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

hence
ex G being Homomorphism of (product F),(product <*H,K*>) st
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;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

( 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