let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds deg t >= height t
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X)) holds deg t >= height t
let t be Element of (Free (S,X)); :: thesis: deg t >= height t
defpred S₁[ Element of (Free (S,X))] means deg $1 >= height $1;
A1: for s being SortSymbol of S
for x being Element of X . s holds S₁[x -term ] by TREES_1:42;
A2: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]

proof

let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) implies S₁[o -term p] )
assume A3: for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ; :: thesis: S₁[o -term p]

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

suppose the_arity_of o = {} ; :: thesis: S₁[o -term p]

hence S₁[o -term p] by Th20; :: thesis: verum

end;

suppose A4: the_arity_of o <> {} ; :: thesis: S₁[o -term p]

set i = the Element of dom (the_arity_of o);
dom (the_arity_of o) <> {} by A4;
then A9: ( the Element of dom (the_arity_of o) in dom (the_arity_of o) & dom (the_arity_of o) = dom p ) by MSUALG_3:6;
then ( p /. the Element of dom (the_arity_of o) = p . the Element of dom (the_arity_of o) & p . the Element of dom (the_arity_of o) in rng p ) by PARTFUN1:def 6, FUNCT_1:def 3;
then height (p /. the Element of dom (the_arity_of o)) in { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } ;
then reconsider I = { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } as non empty finite natural-membered set by Th25;
reconsider n = union I as Nat ;
union I in I by SIMPLEX0:9;
then consider t1 being Element of (Free (S,X)) such that
A7: ( n = height t1 & t1 in rng p ) ;
consider i being object such that
A8: ( i in dom p & t1 = p . i ) by A7, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A8;
A5: height (o -term p) = n + 1 by A4, Th26;
deffunc H₁( object ) -> Nat = deg (p /. $1);
consider g being Function such that
A6: ( dom g = dom (the_arity_of o) & ( for i being object st i in dom (the_arity_of o) holds
g . i = H₁(i) ) ) from FUNCT_1:sch 3();
dom g = Seg (len (the_arity_of o)) by A6, FINSEQ_1:def 3;
then reconsider g = g as FinSequence by FINSEQ_1:def 2;
rng g c= NAT

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng g or a in NAT )
assume a in rng g ; :: thesis: a in NAT
then consider b being object such that
B2: ( b in dom g & a = g . b ) by FUNCT_1:def 3;
a = H₁(b) by A6, B2;
hence a in NAT ; :: thesis: verum

end;

then reconsider g = g as FinSequence of NAT by FINSEQ_1:def 4;

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
g . 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
g . i = deg t
let t be Element of (Free (S,X)); :: thesis: ( i in dom (the_arity_of o) & t = p . i implies g . i = deg t )
assume ( i in dom (the_arity_of o) & t = p . i ) ; :: thesis: g . i = deg t
then ( t = p /. i & g . i = H₁(i) ) by A6, A9, PARTFUN1:def 6;
hence g . i = deg t ; :: thesis: verum

end;

then B3: deg (o -term p) = (Sum g) + 1 by A6, Th29;
( Sum g >= g . i & g . i = H₁(i) & H₁(i) = deg t1 & deg t1 >= n ) by A3, A7, A8, A9, A6, PARTFUN1:def 6, POLYNOM3:4;
then Sum g >= n by XXREAL_0:2;
hence deg (o -term p) >= height (o -term p) by B3, A5, XREAL_1:6; :: thesis: verum

end;

end;

end;

thus S₁[t] from MSAFREE5:sch 2(A1, A2); :: thesis: verum