set q = Sgm (p " {x});

per cases ( not 1 in dom (Sgm (p " {x})) or 1 in dom (Sgm (p " {x})) ) ;

suppose not 1 in dom (Sgm (p " {x})) ; :: thesis: (Sgm (p " {x})) . 1 is Element of NAT

then (Sgm (p " {x})) . 1 = 0 by FUNCT_1:def 2;
hence (Sgm (p " {x})) . 1 is Element of NAT ; :: thesis: verum

end;

suppose A1: 1 in dom (Sgm (p " {x})) ; :: thesis: (Sgm (p " {x})) . 1 is Element of NAT

A2: rng (Sgm (p " {x})) c= NAT by FINSEQ_1:def 4;
(Sgm (p " {x})) . 1 in rng (Sgm (p " {x})) by A1, FUNCT_1:def 3;
hence (Sgm (p " {x})) . 1 is Element of NAT by A2; :: thesis: verum

end;

end;