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