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