let f be Relation; :: thesis: ( rng f is natural-membered iff f is natural-valued )
thus ( rng f is natural-membered implies f is natural-valued ) :: thesis: ( f is natural-valued implies rng f is natural-membered )
proof
set E = (rng f) \/ NAT;
reconsider X = rng f as Subset of ((rng f) \/ NAT) by XBOOLE_1:7;
reconsider Y = NAT as Subset of ((rng f) \/ NAT) by XBOOLE_1:7;
assume rng f is natural-membered ; :: thesis: f is natural-valued
then for x being Element of (rng f) \/ NAT st x in rng f holds
x in NAT by ORDINAL1:def 12;
then X c= Y by SUBSET_1:2;
hence f is natural-valued by VALUED_0:def 6; :: thesis: verum
end;
thus ( f is natural-valued implies rng f is natural-membered ) ; :: thesis: verum