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
for phi1, phi2 being Homomorphism of G,(product F) st ( for i being Element of I holds f . i = (proj (F,i)) * phi1 ) & ( for i being Element of I holds f . i = (proj (F,i)) * phi2 ) holds
phi1 = phi2
let F be Group-Family of I; :: thesis: for G being Group
for f being Homomorphism-Family of G,F
for phi1, phi2 being Homomorphism of G,(product F) st ( for i being Element of I holds f . i = (proj (F,i)) * phi1 ) & ( for i being Element of I holds f . i = (proj (F,i)) * phi2 ) holds
phi1 = phi2
let G be Group; :: thesis: for f being Homomorphism-Family of G,F
for phi1, phi2 being Homomorphism of G,(product F) st ( for i being Element of I holds f . i = (proj (F,i)) * phi1 ) & ( for i being Element of I holds f . i = (proj (F,i)) * phi2 ) holds
phi1 = phi2
let f be Homomorphism-Family of G,F; :: thesis: for phi1, phi2 being Homomorphism of G,(product F) st ( for i being Element of I holds f . i = (proj (F,i)) * phi1 ) & ( for i being Element of I holds f . i = (proj (F,i)) * phi2 ) holds
phi1 = phi2
let phi1, phi2 be Homomorphism of G,(product F); :: thesis: ( ( for i being Element of I holds f . i = (proj (F,i)) * phi1 ) & ( for i being Element of I holds f . i = (proj (F,i)) * phi2 ) implies phi1 = phi2 )
assume A1: for i being Element of I holds f . i = (proj (F,i)) * phi1 ; :: thesis: ( ex i being Element of I st not f . i = (proj (F,i)) * phi2 or phi1 = phi2 )
assume A2: for i being Element of I holds f . i = (proj (F,i)) * phi2 ; :: thesis: phi1 = phi2
for g being Element of G holds phi1 . g = phi2 . g

proof

let g be Element of G; :: thesis: phi1 . g = phi2 . g
( phi1 . g is Element of product (Carrier F) & phi2 . g is Element of product (Carrier F) ) by GROUP_7:def 2;
then B1: ( dom (phi1 . g) = I & dom (phi2 . g) = I ) by PARTFUN1:def 2;
for j being Element of I holds (phi1 . g) . j = (phi2 . g) . j

proof

let j be Element of I; :: thesis: (phi1 . g) . j = (phi2 . g) . j
C2: (f . j) . g = ((proj (F,j)) * phi1) . g by A1
.= (proj (F,j)) . (phi1 . g) by FUNCT_2:15
.= (phi1 . g) . j by Def13 ;
(f . j) . g = ((proj (F,j)) * phi2) . g by A2
.= (proj (F,j)) . (phi2 . g) by FUNCT_2:15
.= (phi2 . g) . j by Def13 ;
hence (phi1 . g) . j = (phi2 . g) . j by C2; :: thesis: verum

end;

hence phi1 . g = phi2 . g by B1; :: thesis: verum

end;

hence phi1 = phi2 by FUNCT_2:def 8; :: thesis: verum