let S be non void Signature; :: thesis: for X being V8() ManySortedSet of the carrier of S
for A being MSSubset of () holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds
(Sym (o,X)) -tree p in A . )

let X be V8() ManySortedSet of the carrier of S; :: thesis: for A being MSSubset of () holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds
(Sym (o,X)) -tree p in A . )

set A = FreeMSA X;
let T be MSSubset of (); :: thesis: ( T is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . )

hereby :: thesis: ( ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . ) implies T is opers_closed )
assume A1: T is opers_closed ; :: thesis: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T .

let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T .

let p be ArgumentSeq of Sym (o,X); :: thesis: ( rng p c= Union T implies (Sym (o,X)) -tree p in T . )
T is_closed_on o by A1;
then A2: rng ((Den (o,())) | (((T #) * the Arity of S) . o)) c= (T * the ResultSort of S) . o ;
A3: p is Element of Args (o,()) by INSTALG1:1;
A4: dom p = dom () by MSATERM:22;
A5: dom T = the carrier of S by PARTFUN1:def 2;
assume A6: rng p c= Union T ; :: thesis: (Sym (o,X)) -tree p in T .
A7: now :: thesis: for x being object st x in dom () holds
p . x in (T * ()) . x
let x be object ; :: thesis: ( x in dom () implies p . x in (T * ()) . x )
assume A8: x in dom () ; :: thesis: p . x in (T * ()) . x
then reconsider i = x as Nat ;
reconsider t = p . i as Term of S,X by ;
A9: ( the_sort_of t = () . x & (T * ()) . x = T . (() . x) ) by ;
p . x in rng p by ;
then consider y being object such that
A10: y in dom T and
A11: p . x in T . y by ;
T c= the Sorts of () by PBOOLE:def 18;
then T . y c= the Sorts of () . y by A10;
hence p . x in (T * ()) . x by A10, A11, A9, Th7; :: thesis: verum
end;
rng () c= dom T by A5;
then dom (T * ()) = dom () by RELAT_1:27;
then A12: p in product (T * ()) by ;
A13: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15
.= (T #) . () by MSUALG_1:def 1
.= product (T * ()) by FINSEQ_2:def 5 ;
then A14: ((Den (o,())) | (((T #) * the Arity of S) . o)) . p = (Den (o,())) . p by ;
dom (Den (o,())) = Args (o,()) by FUNCT_2:def 1;
then p in dom ((Den (o,())) | (((T #) * the Arity of S) . o)) by ;
then A15: (Den (o,())) . p in rng ((Den (o,())) | (((T #) * the Arity of S) . o)) by ;
(T * the ResultSort of S) . o = T . ( the ResultSort of S . o) by FUNCT_2:15
.= T . by MSUALG_1:def 2 ;
then ( [o, the carrier of S] = Sym (o,X) & (Den (o,())) . p in T . ) by ;
hence (Sym (o,X)) -tree p in T . by ; :: thesis: verum
end;
assume A16: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . ; :: thesis: T is opers_closed
let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis:
let x be object ; :: according to TARSKI:def 3,MSUALG_2:def 5 :: thesis: ( not x in proj2 ((Den (o,())) | (( the Arity of S * (T #)) . o)) or x in ( the ResultSort of S * T) . o )
A17: (T * the ResultSort of S) . o = T . ( the ResultSort of S . o) by FUNCT_2:15
.= T . by MSUALG_1:def 2 ;
assume x in rng ((Den (o,())) | (((T #) * the Arity of S) . o)) ; :: thesis: x in ( the ResultSort of S * T) . o
then consider y being object such that
A18: y in dom ((Den (o,())) | (((T #) * the Arity of S) . o)) and
A19: x = ((Den (o,())) | (((T #) * the Arity of S) . o)) . y by FUNCT_1:def 3;
y in dom (Den (o,())) by ;
then reconsider y = y as Element of Args (o,()) ;
reconsider p = y as ArgumentSeq of Sym (o,X) by INSTALG1:1;
A20: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15
.= (T #) . () by MSUALG_1:def 1
.= product (T * ()) by FINSEQ_2:def 5 ;
A21: rng p c= Union T
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in Union T )
A22: dom T = the carrier of S by PARTFUN1:def 2;
assume z in rng p ; :: thesis: z in Union T
then consider a being object such that
A23: a in dom p and
A24: z = p . a by FUNCT_1:def 3;
A25: dom p = dom (T * ()) by ;
then A26: ( z in (T * ()) . a & (T * ()) . a = T . (() . a) ) by ;
rng () c= the carrier of S ;
then dom (T * ()) = dom () by ;
then (the_arity_of o) . a in rng () by ;
hence z in Union T by ; :: thesis: verum
end;
x = (Den (o,())) . y by
.= [o, the carrier of S] -tree y by INSTALG1:3
.= (Sym (o,X)) -tree p by MSAFREE:def 9 ;
hence x in ( the ResultSort of S * T) . o by ; :: thesis: verum