let k be natural number ; :: thesis: Sgm (Seg k) = idseq k
defpred S₁[ Element of NAT ] means Sgm (Seg $1) = idseq $1;
A1: k is Element of NAT by ORDINAL1:def 13;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1] by Lm5;
A3: S₁[ 0 ] by Th49;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A2);
hence Sgm (Seg k) = idseq k by A1; :: thesis: verum