let i be Nat; :: thesis: for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= (i + 1) = (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T))
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 holds T deg<= (i + 1) = (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T))
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 holds T deg<= (i + 1) = (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T))
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: T deg<= (i + 1) = (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T))
set I = { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } ;
thus T deg<= (i + 1) c= (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T)) :: according to XBOOLE_0:def 10 :: thesis: (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T)) c= T deg<= (i + 1)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in T deg<= (i + 1) or a in (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T)) )
assume a in T deg<= (i + 1) ; :: thesis: a in (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T))
then consider r being Element of T such that
A2: ( a = r & deg r <= i + 1 ) ;
reconsider t = r as Element of (Free (S,X)) by MSAFREE4:39;

per cases ( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p ) by Th16;

suppose ex s being SortSymbol of S ex x being Element of X . s st t = x -term ; :: thesis: a in (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T))

then t in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } ;
then t in T deg<= 0 by Th11;
hence a in (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p ; :: thesis: a in (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T))

then consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A3: t = o -term p ;
deffunc H₁( object ) -> Nat = deg (p /. $1);
consider f being Function such that
A4: ( dom f = dom p & ( for a being object st a in dom p holds
f . a = H₁(a) ) ) from FUNCT_1:sch 3();
dom f = Seg (len p) by A4, FINSEQ_1:def 3;
then reconsider f = f as FinSequence by FINSEQ_1:def 2;
rng f c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider x being object such that
A5: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
y = H₁(x) by A4, A5;
hence y in NAT ; :: thesis: verum

end;

then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
A6: dom f = dom (the_arity_of o) by A4, MSUALG_3:6;

A8: now :: thesis: for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t

let i be Nat; :: thesis: for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t
let t be Element of (Free (S,X)); :: thesis: ( i in dom (the_arity_of o) & t = p . i implies f . i = deg t )
assume A7: ( i in dom (the_arity_of o) & t = p . i ) ; :: thesis: f . i = deg t
then t = p /. i by A4, A6, PARTFUN1:def 6;
hence f . i = deg t by A4, A6, A7; :: thesis: verum

end;

then deg t = (Sum f) + 1 by A3, A4, Th29, MSUALG_3:6;
then Sum f <= i by A2, XREAL_1:6;
then ( t in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } & t in Union the Sorts of T ) by A3, A6, A8;
then t in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T) by XBOOLE_0:def 4;
hence a in (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A10: T deg<= 0 c= T deg<= (i + 1) by Th10b;
{ (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T) c= T deg<= (i + 1)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T) or a in T deg<= (i + 1) )
assume A14: a in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T) ; :: thesis: a in T deg<= (i + 1)
then A11: ( a in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } & a in Union the Sorts of T ) by XBOOLE_0:def 4;
reconsider r = a as Element of T by A14, XBOOLE_0:def 4;
consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A12: ( a = o -term p & ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) ) by A11;
consider f being FinSequence of NAT such that
A13: ( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) by A12;
( i + 1 >= (Sum f) + 1 & (Sum f) + 1 = deg (o -term p) & a in T & deg r = deg (o -term p) ) by A14, A12, A13, Th29, XREAL_1:6, XBOOLE_0:def 4;
hence a in T deg<= (i + 1) ; :: thesis: verum

end;

hence (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T)) c= T deg<= (i + 1) by A10, XBOOLE_1:8; :: thesis: verum