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 i being Element of I holds f . i = (proj (F,i)) * phi
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 i being Element of I holds f . i = (proj (F,i)) * phi
let G be Group; :: thesis: for f being Homomorphism-Family of G,F ex phi being Homomorphism of G,(product F) st
for i being Element of I holds f . i = (proj (F,i)) * phi
let f be Homomorphism-Family of G,F; :: thesis: ex phi being Homomorphism of G,(product F) st
for i being Element of I holds f . i = (proj (F,i)) * phi
consider phi being Homomorphism of G,(product F) such that
A1: for g being Element of G
for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g) by Th39;
take phi ; :: thesis: for i being Element of I holds f . i = (proj (F,i)) * phi
let i be Element of I; :: thesis: f . i = (proj (F,i)) * phi
for g being Element of G holds ((proj (F,i)) * phi) . g = (f . i) . g

proof

let g be Element of G; :: thesis: ((proj (F,i)) * phi) . g = (f . i) . g
(f . i) . g = (proj (F,i)) . (phi . g) by A1
.= ((proj (F,i)) * phi) . g by FUNCT_2:15 ;
hence (f . i) . g = ((proj (F,i)) * phi) . g ; :: thesis: verum

end;

hence f . i = (proj (F,i)) * phi by FUNCT_2:def 8; :: thesis: verum