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;