let F be Function; :: thesis: for i being set st i in dom F holds
( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) )
let i be set ; :: thesis: ( i in dom F implies ( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) ) )
assume A1: i in dom F ; :: thesis: ( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) )
thus A0: rng (proj (F,i)) c= F . i :: thesis: ( product F <> {} implies rng (proj (F,i)) = 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 3;
f9 in product F by A3;
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 16;
hence x in F . i by A1, A4, A5, A6; :: thesis: verum

end;

assume A2: product F <> {} ; :: thesis: rng (proj (F,i)) = F . i
thus rng (proj (F,i)) c= F . i by A0; :: according to XBOOLE_0:def 10 :: thesis: F . i c= rng (proj (F,i))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F . i or x in rng (proj (F,i)) )
set f9 = the Element of product F;
consider f being Function such that
A7: the Element of product F = 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 16;
(f +* (i,x)) . i = x by A1, A8, FUNCT_7:31;
then (proj (F,i)) . (f +* (i,x)) = x by A9, CARD_3:def 16;
hence x in rng (proj (F,i)) by A9, FUNCT_1:def 3; :: thesis: verum