let I be non empty set ; :: thesis: for i being Element of I
for F being Group-Family of I holds proj ((Carrier F),i) is Function of (product (Carrier F)), the carrier of (F . i)
let i be Element of I; :: thesis: for F being Group-Family of I holds proj ((Carrier F),i) is Function of (product (Carrier F)), the carrier of (F . i)
let F be Group-Family of I; :: thesis: proj ((Carrier F),i) is Function of (product (Carrier F)), the carrier of (F . i)
set X = product (Carrier F);
set Y = the carrier of (F . i);
set f = proj ((Carrier F),i);
A1: dom (proj ((Carrier F),i)) = product (Carrier F) by CARD_3:def 16;
for x being object st x in product (Carrier F) holds
(proj ((Carrier F),i)) . x in the carrier of (F . i)

proof

let x be object ; :: thesis: ( x in product (Carrier F) implies (proj ((Carrier F),i)) . x in the carrier of (F . i) )
assume A2: x in product (Carrier F) ; :: thesis: (proj ((Carrier F),i)) . x in the carrier of (F . i)
then reconsider y = x as Element of (product F) by GROUP_7:def 2;
(proj ((Carrier F),i)) . y = y /. i by A1, A2, CARD_3:def 16;
hence (proj ((Carrier F),i)) . x in the carrier of (F . i) ; :: thesis: verum

end;

hence proj ((Carrier F),i) is Function of (product (Carrier F)), the carrier of (F . i) by A1, FUNCT_2:3; :: thesis: verum