consider f being Function such that
A1: f = proj ((Carrier J),i) ;
A2: dom f = product (Carrier J) by A1, CARD_3:def 16
.= the carrier of (product J) by Def3 ;
rng f c= the carrier of (J . i)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of (J . i) )
assume y in rng f ; :: thesis: y in the carrier of (J . i)
then consider x being object such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def 3;
reconsider x = x as Element of (product J) by A2, A3;
f . x = x . i by A1, A3, CARD_3:def 16;
hence y in the carrier of (J . i) by A4; :: thesis: verum

end;

hence proj ((Carrier J),i) is Function of (product J),(J . i) by A1, A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum