let e be Element of doms F; :: thesis: e is NAT -valued

per cases ( doms F is empty or not doms F is empty ) ;

suppose doms F is empty ; :: thesis: e is NAT -valued

then e = {} by SUBSET_1:def 1;
hence e is NAT -valued ; :: thesis: verum

end;

suppose A1: not doms F is empty ; :: thesis: e is NAT -valued

rng e c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng e or y in NAT )
assume A2: y in rng e ; :: thesis: y in NAT
consider x being object such that
A3: ( x in dom e & e . x = y ) by A2, FUNCT_1:def 3;
e . x in dom (F . x) by A1, Th47, A3;
hence y in NAT by A3; :: thesis: verum

end;

hence e is NAT -valued by RELAT_1:def 19; :: thesis: verum

end;

end;