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

proof

let y be set ; :: 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 set such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def 5;
reconsider x = x as Element of (product J) by A2, A3;
f . x = x . i by A1, A3, PRALG_3:def 2;
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:11; :: thesis: verum