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