let k be natural number ; :: thesis: Sgm (Seg k) = idseq k
defpred S₁[ Nat] means Sgm (Seg $1) = idseq $1;
A2: for k being Nat st S₁[k] holds
S₁[k + 1] by Lm5;
A3: S₁[ 0 ] by Th49;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A2);
hence Sgm (Seg k) = idseq k ; :: thesis: verum