let A be QC-alphabet ; :: thesis: for n being Nat
for t being QC-symbol of A holds t <= t + n
let n be Nat; :: thesis: for t being QC-symbol of A holds t <= t + n
let t be QC-symbol of A; :: thesis: t <= t + n
defpred S₁[ Nat] means t <= t + $1;
A1: S₁[ 0 ]

proof

consider f being sequence of (QC-symbols A) such that
A2: ( t + 0 = f . 0 & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) by Def40;
thus S₁[ 0 ] by A2, Th22; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: t <= t + k ; :: thesis: S₁[k + 1]
consider f being sequence of (QC-symbols A) such that
A5: ( t + (k + 1) = f . (k + 1) & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) by Def40;
f . k = t + k by A5, Def40;
then f . (k + 1) = (t + k) ++ by A5;
then t < t + (k + 1) by A5, A4, Th27, Th29;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence t <= t + n ; :: thesis: verum