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