let I0, I be non empty finite set ; 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; 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; 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; 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; 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; ( 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 )
; 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;
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;
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;
( h = G0 . x0 & x0 in product F0 implies G . (x0 +* (q .--> k)) = <*h,k*> )
assume A9:
(
h = G0 . x0 &
x0 in product F0 )
;
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;
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; verum