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