let m be Nat; :: according to RVSUM_3:def 1 :: thesis: ( not m in dom (Sgm X) or not (Sgm X) . m <= 0 )
assume m in dom (Sgm X) ; :: thesis: not (Sgm X) . m <= 0
then (Sgm X) . m in X by A1, FUNCT_1:def 3;
then (Sgm X) . m is prime by NEWTON:def 6;
hence (Sgm X) . m > 0 ; :: thesis: verum