let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) holds
( { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is natural-membered & { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite & union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat )
let X be V5() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) holds
( { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is natural-membered & { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite & union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat )
let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) holds
( { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is natural-membered & { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite & union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat )
let p be Element of Args (o,(Free (S,X))); :: thesis: ( { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is natural-membered & { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite & union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat )
set I = { (height t) where t is Element of (Free (S,X)) : t in rng p } ;
thus A2: { (height t) where t is Element of (Free (S,X)) : t in rng p } is natural-membered :: thesis: ( { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite & union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat )

proof

let a be object ; :: according to MEMBERED:def 6 :: thesis: ( not a in { (height t) where t is Element of (Free (S,X)) : t in rng p } or a is natural )
assume a in { (height t) where t is Element of (Free (S,X)) : t in rng p } ; :: thesis: a is natural
then ex t1 being Element of (Free (S,X)) st
( a = height t1 & t1 in rng p ) ;
hence a is natural ; :: thesis: verum

end;

deffunc H₁( Element of (Free (S,X))) -> Nat = height $1;
A3: rng p is finite ;
thus { H₁(t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite from FRAENKEL:sch 21(A3); :: thesis: union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat
then reconsider I = { (height t) where t is Element of (Free (S,X)) : t in rng p } as finite natural-membered set by A2;
union I is Nat ;
hence union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat ; :: thesis: verum