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 height<= (i + 1) = (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (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 height<= (i + 1) = (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (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 height<= (i + 1) = (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T))
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: T height<= (i + 1) = (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (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))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } ;
thus T height<= (i + 1) c= (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T)) :: according to XBOOLE_0:def 10 :: thesis: (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T)) c= T height<= (i + 1)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in T height<= (i + 1) or a in (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T)) )
assume a in T height<= (i + 1) ; :: thesis: a in (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T))
then consider t being Element of (Free (S,X)) such that
A2: ( a = t & t in T & height t <= i + 1 ) ;

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 height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (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 { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } by XBOOLE_0:def 3;
then t in T height<= 0 by Th12;
hence a in (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (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 height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (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 ;
reconsider n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } as Nat by Th25;

per cases ( the_arity_of o = {} or the_arity_of o <> {} ) ;

suppose the_arity_of o = {} ; :: thesis: a in (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T))

then t in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } by A2, A3;
then t in { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) } by XBOOLE_0:def 3;
then t in T height<= 0 by Th12;
hence a in (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

suppose the_arity_of o <> {} ; :: thesis: a in (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T))

then height t = n + 1 by A3, Th26;
then Segm n c= Segm i by A2, XREAL_1:6, NAT_1:39;
then ( t in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } & t in Union the Sorts of T ) by A2, A3;
then t in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T) by XBOOLE_0:def 4;
hence a in (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

end;

A10: T height<= 0 c= T height<= (i + 1) by Th10c;
{ (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T) c= T height<= (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))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T) or a in T height<= (i + 1) )
assume A15: a in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T) ; :: thesis: a in T height<= (i + 1)
then ( a in { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } & a in Union the Sorts of T ) by XBOOLE_0:def 4;
then consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A12: ( a = o -term p & union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i ) ;
reconsider n = union { (height t) where t is Element of (Free (S,X)) : t in rng p } as Nat by Th25;
A13: Segm n c= Segm i by A12;
A14: a in T by A15, XBOOLE_0:def 4;

per cases ( the_arity_of o <> {} or the_arity_of o = {} ) ;

suppose the_arity_of o <> {} ; :: thesis: a in T height<= (i + 1)

then ( height (o -term p) = n + 1 & n + 1 <= i + 1 ) by A13, Th26, NAT_1:39, XREAL_1:6;
hence a in T height<= (i + 1) by A12, A14; :: thesis: verum

end;

suppose the_arity_of o = {} ; :: thesis: a in T height<= (i + 1)

then ( height (o -term p) = 0 & 0 <= i + 1 ) by Th20;
hence a in T height<= (i + 1) by A12, A14; :: thesis: verum

end;

end;

end;

hence (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T)) c= T height<= (i + 1) by A10, XBOOLE_1:8; :: thesis: verum