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)

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
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:

end;