set ox = o . x;

per cases ( x in dom o or not x in dom o ) ;

suppose A1: x in dom o ; :: thesis: o . x is natural-valued

rng (o . x) c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (o . x) or y in NAT )
assume y in rng (o . x) ; :: thesis: y in NAT
then consider z being object such that
A2: ( z in dom (o . x) & (o . x) . z = y ) by FUNCT_1:def 3;
y in Values o by A1, A2, Th1;
then y in D by Def7;
hence y in NAT by ORDINAL1:def 12; :: thesis: verum

end;

hence o . x is natural-valued by VALUED_0:def 6; :: thesis: verum

end;

suppose not x in dom o ; :: thesis: o . x is natural-valued

hence o . x is natural-valued by FUNCT_1:def 2; :: thesis: verum

end;

end;