let S be non void Signature; :: thesis:
let X be V5() ManySortedSet of ; :: thesis:
set A = FreeMSA X;
let T be MSSubset of (FreeMSA X); :: thesis:

hereby :: thesis:

assume A1: T is opers_closed ; :: thesis:
let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of Sym o,X; :: thesis:
T is_closed_on o by A1, MSUALG_2:def 7;
then A2: rng ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) c= (T * the ResultSort of S) . o by MSUALG_2:def 6;
A3: ((T # ) * the Arity of S) . o = (T # ) . (the Arity of S . o) by FUNCT_2:21
.= (T # ) . (the_arity_of o) by MSUALG_1:def 6
.= product (T * (the_arity_of o)) by PBOOLE:def 19 ;
A4: ( p is Element of Args o,(FreeMSA X) & dom (Den o,(FreeMSA X)) = Args o,(FreeMSA X) ) by FUNCT_2:def 1, INSTALG1:2;
A5: (T * the ResultSort of S) . o = T . (the ResultSort of S . o) by FUNCT_2:21
.= T . (the_result_sort_of o) by MSUALG_1:def 7 ;
A6: [o,the carrier of S] = Sym o,X by MSAFREE:def 11;
assume A7: rng p c= Union T ; :: thesis:
A8: dom p = dom (the_arity_of o) by MSATERM:22;
A9: dom T = the carrier of S by PARTFUN1:def 4;
then rng (the_arity_of o) c= dom T ;
then A10: dom (T * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46;

now

let x be set ; :: thesis:
assume A11: x in dom (the_arity_of o) ; :: thesis:
then p . x in rng p by A8, FUNCT_1:def 5;
then consider y being set such that
A12: ( y in dom T & p . x in T . y ) by A7, CARD_5:10;
reconsider i = x as Nat by A11;
reconsider t = p . i as Term of S,X by A8, A11, MSATERM:22;
A13: the_sort_of t = (the_arity_of o) . x by A8, A11, MSATERM:23;
A14: (T * (the_arity_of o)) . x = T . ((the_arity_of o) . x) by A11, FUNCT_1:23;
T c= the Sorts of (FreeMSA X) by PBOOLE:def 23;
then T . y c= the Sorts of (FreeMSA X) . y by A9, A12, PBOOLE:def 5;
hence p . x in (T * (the_arity_of o)) . x by A9, A12, A13, A14, Th8; :: thesis:

end;

then p in product (T * (the_arity_of o)) by A8, A10, CARD_3:18;
then ( p in dom ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) & ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) . p = (Den o,(FreeMSA X)) . p ) by A3, A4, FUNCT_1:72, RELAT_1:86;
then (Den o,(FreeMSA X)) . p in rng ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) by FUNCT_1:def 5;
then (Den o,(FreeMSA X)) . p in T . (the_result_sort_of o) by A2, A5;
hence (Sym o,X) -tree p in T . (the_result_sort_of o) by A4, A6, INSTALG1:4; :: thesis:

end;

assume A15: 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 . (the_result_sort_of o) ; :: thesis:
let o be OperSymbol of S; :: according to MSUALG_2:def 7 :: thesis:
let x be set ; :: according to TARSKI:def 3,MSUALG_2:def 6 :: thesis:
assume x in rng ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) ; :: thesis:
then consider y being set such that
A16: y in dom ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) and
A17: x = ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) . y by FUNCT_1:def 5;
A18: ((T # ) * the Arity of S) . o = (T # ) . (the Arity of S . o) by FUNCT_2:21
.= (T # ) . (the_arity_of o) by MSUALG_1:def 6
.= product (T * (the_arity_of o)) by PBOOLE:def 19 ;
A19: (T * the ResultSort of S) . o = T . (the ResultSort of S . o) by FUNCT_2:21
.= T . (the_result_sort_of o) by MSUALG_1:def 7 ;
( the Sorts of (FreeMSA X) is MSSubset of (FreeMSA X) & T c= the Sorts of (FreeMSA X) ) by PBOOLE:def 23;
then ((T # ) * the Arity of S) . o c= ((the Sorts of (FreeMSA X) # ) * the Arity of S) . o by MSUALG_2:3;
then A20: ( dom ((Den o,(FreeMSA X)) | (((T # ) * the Arity of S) . o)) c= ((T # ) * the Arity of S) . o & ((T # ) * the Arity of S) . o c= Args o,(FreeMSA X) ) by MSUALG_1:def 9, RELAT_1:87;
reconsider y = y as Element of Args o,(FreeMSA X) by A16;
reconsider p = y as ArgumentSeq of Sym o,X by INSTALG1:2;
A21: x = (Den o,(FreeMSA X)) . y by A16, A17, FUNCT_1:70
.= [o,the carrier of S] -tree y by INSTALG1:4
.= (Sym o,X) -tree p by MSAFREE:def 11 ;
rng p c= Union T

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng p ; :: thesis:
then consider a being set such that
A22: ( a in dom p & z = p . a ) by FUNCT_1:def 5;
A23: ( dom T = the carrier of S & rng (the_arity_of o) c= the carrier of S ) by PARTFUN1:def 4;
then A24: ( dom (T * (the_arity_of o)) = dom (the_arity_of o) & dom p = dom (T * (the_arity_of o)) ) by A16, A18, A20, CARD_3:18, RELAT_1:46;
then (the_arity_of o) . a in rng (the_arity_of o) by A22, FUNCT_1:def 5;
then ( z in (T * (the_arity_of o)) . a & (the_arity_of o) . a in the carrier of S & (T * (the_arity_of o)) . a = T . ((the_arity_of o) . a) ) by A16, A18, A20, A22, A24, CARD_3:18, FUNCT_1:22;
hence z in Union T by A23, CARD_5:10; :: thesis:

end;

hence x in (the ResultSort of S * T) . o by A15, A19, A21; :: thesis: