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 A2: rng (proj (F,i)) c= F . i :: thesis: ( product F <> {} implies rng (proj (F,i)) = F . i )

proof

let x be object ; :: 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 object 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 object 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 A7: product F <> {} ; :: thesis: rng (proj (F,i)) = F . i
thus rng (proj (F,i)) c= F . i by A2; :: according to XBOOLE_0:def 10 :: thesis: F . i c= rng (proj (F,i))
let x be object ; :: 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
A8: the Element of product F = f and
A9: dom f = dom F and
for x being object st x in dom F holds
f . x in F . x by A7, CARD_3:def 5;
assume x in F . i ; :: thesis: x in rng (proj (F,i))
then f +* (i,x) in product F by A7, A8, Th2;
then A10: f +* (i,x) in dom (proj (F,i)) by CARD_3:def 16;
(f +* (i,x)) . i = x by A1, A9, FUNCT_7:31;
then (proj (F,i)) . (f +* (i,x)) = x by A10, CARD_3:def 16;
hence x in rng (proj (F,i)) by A10, FUNCT_1:def 3; :: thesis: verum