let I be non empty set ; :: thesis: for i being Element of I
for F being Group-Family of I holds proj (F,i) = proj ((Carrier F),i)
let i be Element of I; :: thesis: for F being Group-Family of I holds proj (F,i) = proj ((Carrier F),i)
let F be Group-Family of I; :: thesis: proj (F,i) = proj ((Carrier F),i)
set X = product (Carrier F);
set Y = the carrier of (F . i);
product (Carrier F) = the carrier of (product F) by GROUP_7:def 2;
then A1: ( proj ((Carrier F),i) is Function of (product (Carrier F)), the carrier of (F . i) & proj (F,i) is Function of (product (Carrier F)), the carrier of (F . i) ) by Th31;
for x being Element of product (Carrier F) holds (proj (F,i)) . x = (proj ((Carrier F),i)) . x

proof

let x be Element of product (Carrier F); :: thesis: (proj (F,i)) . x = (proj ((Carrier F),i)) . x
x is Element of (product F) by GROUP_7:def 2;
hence (proj (F,i)) . x = (proj ((Carrier F),i)) . x by Th32; :: thesis: verum

end;

hence proj (F,i) = proj ((Carrier F),i) by A1, FUNCT_2:63; :: thesis: verum