let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for i being Nat holds T deg<= i c= (Free (S,X)) deg<= i
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for i being Nat holds T deg<= i c= (Free (S,X)) deg<= i
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for i being Nat holds T deg<= i c= (Free (S,X)) deg<= i
defpred S₁[ Nat] means T deg<= $1 c= (Free (S,X)) deg<= $1;
( T deg<= 0 = Union (FreeGen T) & (Free (S,X)) deg<= 0 = Union (FreeGen (Free (S,X))) ) by Th44;
then A0: S₁[ 0 ] ;

A1: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T deg<= (i + 1) or x in (Free (S,X)) deg<= (i + 1) )
assume x in T deg<= (i + 1) ; :: thesis: x in (Free (S,X)) deg<= (i + 1)
then consider r being Element of T such that
A3: ( x = r & deg r <= i + 1 ) ;
reconsider t = r as Element of (Free (S,X)) by MSAFREE4:39;
deg t = deg r ;
hence x in (Free (S,X)) deg<= (i + 1) by A3; :: thesis: verum

end;

end;

thus for i being Nat holds S₁[i] from NAT_1:sch 2(A0, A1); :: thesis: verum