let I be non empty set ; :: thesis: for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F ex phi being Homomorphism of G,(product F) st
for g being Element of G
for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g)
let F be Group-Family of I; :: thesis: for G being Group
for f being Homomorphism-Family of G,F ex phi being Homomorphism of G,(product F) st
for g being Element of G
for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g)
let G be Group; :: thesis: for f being Homomorphism-Family of G,F ex phi being Homomorphism of G,(product F) st
for g being Element of G
for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g)
let f be Homomorphism-Family of G,F; :: thesis: ex phi being Homomorphism of G,(product F) st
for g being Element of G
for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g)
defpred S₁[ object , object ] means ex g0 being Element of (product F) st
( $2 = g0 & ( for j being Element of I holds (f . j) . $1 = g0 . j ) );
deffunc H₁() -> set = the carrier of G;
A1: for x being object st x in H₁() holds
ex y being object st
( y in the carrier of (product F) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in H₁() implies ex y being object st
( y in the carrier of (product F) & S₁[x,y] ) )
assume x in H₁() ; :: thesis: ex y being object st
( y in the carrier of (product F) & S₁[x,y] )
then reconsider xx = x as Element of G ;
defpred S₂[ object , object ] means ex i being Element of I st
( i = $1 & $2 = (f . i) . xx );
B1: for i, y1, y2 being object st i in I & S₂[i,y1] & S₂[i,y2] holds
y1 = y2 ;
B2: for i being object st i in I holds
ex y being object st S₂[i,y]

proof

let i be object ; :: thesis: ( i in I implies ex y being object st S₂[i,y] )
assume i in I ; :: thesis: ex y being object st S₂[i,y]
then reconsider ii = i as Element of I ;
consider y being object such that
C1: y = (f . ii) . xx ;
take y ; :: thesis: S₂[i,y]
thus S₂[i,y] by C1; :: thesis: verum

end;

consider y being Function such that
B3: dom y = I and
B4: for j being object st j in I holds
S₂[j,y . j] from FUNCT_1:sch 2(B1, B2);
take y ; :: thesis: ( y in the carrier of (product F) & S₁[x,y] )
thus y in the carrier of (product F) :: thesis: S₁[x,y]

proof

C1: dom y = dom (Carrier F) by B3, PARTFUN1:def 2;
for i being Element of I holds y . i in (Carrier F) . i

proof

let i be Element of I; :: thesis: y . i in (Carrier F) . i
S₂[i,y . i] by B4;
then consider ii being Element of I such that
D1: ( ii = i & y . i = (f . i) . xx ) ;
(Carrier F) . i = the carrier of (F . i) by Th9;
hence y . i in (Carrier F) . i by D1; :: thesis: verum

end;

then for i being object st i in dom (Carrier F) holds
y . i in (Carrier F) . i ;
then y in product (Carrier F) by C1, CARD_3:9;
hence y in the carrier of (product F) by GROUP_7:def 2; :: thesis: verum

end;

then consider g0 being Element of (product F) such that
B5: g0 = y ;
take g0 ; :: thesis: ( y = g0 & ( for j being Element of I holds (f . j) . x = g0 . j ) )
thus y = g0 by B5; :: thesis: for j being Element of I holds (f . j) . x = g0 . j
let j be Element of I; :: thesis: (f . j) . x = g0 . j
S₂[j,g0 . j] by B4, B5;
hence (f . j) . x = g0 . j ; :: thesis: verum

end;

consider phi being Function of H₁(), the carrier of (product F) such that
A2: for x being object st x in H₁() holds
S₁[x,phi . x] from FUNCT_2:sch 1(A1);
reconsider phi = phi as Function of G,(product F) ;
A3: for g being Element of G
for j being Element of I holds (phi . g) . j = (f . j) . g

proof

let g be Element of G; :: thesis: for j being Element of I holds (phi . g) . j = (f . j) . g
let j be Element of I; :: thesis: (phi . g) . j = (f . j) . g
S₁[g,phi . g] by A2;
hence (phi . g) . j = (f . j) . g ; :: thesis: verum

end;

for a, b being Element of G holds phi . (a * b) = (phi . a) * (phi . b)

proof

let a, b be Element of G; :: thesis: phi . (a * b) = (phi . a) * (phi . b)
( phi . (a * b) is Element of product (Carrier F) & (phi . a) * (phi . b) is Element of product (Carrier F) ) by GROUP_7:def 2;
then B1: ( dom (phi . (a * b)) = I & dom ((phi . a) * (phi . b)) = I ) by PARTFUN1:def 2;
for j being Element of I holds (phi . (a * b)) . j = ((phi . a) * (phi . b)) . j

proof

let j be Element of I; :: thesis: (phi . (a * b)) . j = ((phi . a) * (phi . b)) . j
reconsider fj = f . j as Homomorphism of G,(F . j) ;
(phi . (a * b)) . j = fj . (a * b) by A3
.= (fj . a) * (fj . b) by GROUP_6:def 6
.= ((phi . a) /. j) * (fj . b) by A3
.= ((phi . a) /. j) * ((phi . b) /. j) by A3
.= ((phi . a) * (phi . b)) /. j by GROUP_7:1 ;
hence (phi . (a * b)) . j = ((phi . a) * (phi . b)) . j ; :: thesis: verum

end;

hence phi . (a * b) = (phi . a) * (phi . b) by B1; :: thesis: verum

end;

then reconsider phi = phi as Homomorphism of G,(product F) by GROUP_6:def 6;
take phi ; :: thesis: for g being Element of G
for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g)
let g be Element of G; :: thesis: for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g)
for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g)

proof

let j be Element of I; :: thesis: (f . j) . g = (proj (F,j)) . (phi . g)
(f . j) . g = (phi . g) . j by A3;
hence (f . j) . g = (proj (F,j)) . (phi . g) by Def13; :: thesis: verum

end;

hence for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g) ; :: thesis: verum