let x be object ; :: according to VALUED_0:def 12 :: thesis: ( not x in dom (0_ (X,F_Real)) or (0_ (X,F_Real)) . x is natural )
assume x in dom (0_ (X,F_Real)) ; :: thesis: (0_ (X,F_Real)) . x is natural
then (0_ (X,F_Real)) . x = 0. F_Real by POLYNOM1:22
.= 0 ;
hence (0_ (X,F_Real)) . x is natural ; :: thesis: verum