let F be Function; :: thesis: for i being set st i in dom F & product F <> {} holds
rng (proj F,i) = F . i
let i be set ; :: thesis: ( i in dom F & product F <> {} implies rng (proj F,i) = F . i )
assume that
A1: i in dom F and
A2: product F <> {} ; :: thesis: rng (proj F,i) = F . i
thus rng (proj F,i) c= F . i :: according to XBOOLE_0:def 10 :: thesis: F . i c= rng (proj F,i)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (proj F,i) or x in F . i )
assume x in rng (proj F,i) ; :: thesis: x in F . i
then consider f9 being set such that
A3: f9 in dom (proj F,i) and
A4: x = (proj F,i) . f9 by FUNCT_1:def 5;
f9 in product F by A3, CARD_3:def 17;
then consider f being Function such that
A5: f9 = f and
dom f = dom F and
A6: for x being set st x in dom F holds
f . x in F . x by CARD_3:def 5;
(proj F,i) . f = f . i by A3, A5, CARD_3:def 17;
hence x in F . i by A1, A4, A5, A6; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F . i or x in rng (proj F,i) )
consider f9 being Element of product F;
consider f being Function such that
A7: f9 = f and
A8: dom f = dom F and
for x being set st x in dom F holds
f . x in F . x by A2, CARD_3:def 5;
assume x in F . i ; :: thesis: x in rng (proj F,i)
then f +* i,x in product F by A2, A7, Th2;
then A9: f +* i,x in dom (proj F,i) by CARD_3:def 17;
(f +* i,x) . i = x by A1, A8, FUNCT_7:33;
then (proj F,i) . (f +* i,x) = x by A9, CARD_3:def 17;
hence x in rng (proj F,i) by A9, FUNCT_1:def 5; :: thesis: verum