let S be non void Signature; :: thesis: for Y being V5() ManySortedSet of
for X being ManySortedSet of holds S -Terms X,Y is opers_closed
let Y be V5() ManySortedSet of ; :: thesis: for X being ManySortedSet of holds S -Terms X,Y is opers_closed
let X be ManySortedSet of ; :: 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 Th20;
hence S -Terms X,Y is opers_closed by Th21; :: thesis: verum