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