let S be non void Signature; :: thesis: for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed

let Y be V8() ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed

let X be ManySortedSet of the carrier of S; :: thesis: S -Terms (X,Y) is opers_closed

for o being OperSymbol of S

for p being ArgumentSeq of Sym (o,Y) st rng p c= Union (S -Terms (X,Y)) holds

(Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) by Th19;

hence S -Terms (X,Y) is opers_closed by Th20; :: thesis: verum

for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed

let Y be V8() ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed

let X be ManySortedSet of the carrier of S; :: thesis: S -Terms (X,Y) is opers_closed

for o being OperSymbol of S

for p being ArgumentSeq of Sym (o,Y) st rng p c= Union (S -Terms (X,Y)) holds

(Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) by Th19;

hence S -Terms (X,Y) is opers_closed by Th20; :: thesis: verum