set f = b1 -' b2;
rng (b1 -' b2) c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (b1 -' b2) or y in NAT )
assume y in rng (b1 -' b2) ; :: thesis: y in NAT
then consider x being object such that
x in dom (b1 -' b2) and
A1: y = (b1 -' b2) . x by FUNCT_1:def 3;
(b1 -' b2) . x = (b1 . x) -' (b2 . x) by Def6;
hence y in NAT by A1; :: thesis: verum

end;

hence b1 -' b2 is natural-valued ; :: thesis: verum