let S be non void Signature; :: thesis: for Y being non-empty 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 non-empty 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