let S be non void Signature; :: thesis: for X, Y being V5() ManySortedSet of
for t being Term of the carrier of (DTConMSA Y), st variables_in t c= X holds
t is Term of the carrier of (DTConMSA X),
let X, Y be V5() ManySortedSet of ; :: thesis: for t being Term of the carrier of (DTConMSA Y), st variables_in t c= X holds
t is Term of the carrier of (DTConMSA X),
defpred S₁[ DecoratedTree] means ( Y variables_in $1 c= X implies $1 is Term of the carrier of (DTConMSA X), );
let t be Term of the carrier of (DTConMSA Y),; :: thesis: ( variables_in t c= X implies t is Term of the carrier of (DTConMSA X), )
A1: for o being OperSymbol of
for p being ArgumentSeq of Sym o,Y st ( for t being Term of the carrier of (DTConMSA Y), st t in rng p holds
S₁[t] ) holds
S₁[[o,the carrier of S] -tree p]

proof

let o be OperSymbol of ; :: thesis: for p being ArgumentSeq of Sym o,Y st ( for t being Term of the carrier of (DTConMSA Y), st t in rng p holds
S₁[t] ) holds
S₁[[o,the carrier of S] -tree p]
let p be ArgumentSeq of Sym o,Y; :: thesis: ( ( for t being Term of the carrier of (DTConMSA Y), st t in rng p holds
S₁[t] ) implies S₁[[o,the carrier of S] -tree p] )
assume that
A2: for t being Term of the carrier of (DTConMSA Y), st t in rng p & Y variables_in t c= X holds
t is Term of the carrier of (DTConMSA X), and
A3: Y variables_in ([o,the carrier of S] -tree p) c= X ; :: thesis: [o,the carrier of S] -tree p is Term of the carrier of (DTConMSA X),

A4: now

let i be Nat; :: thesis: ( i in dom p implies ex t' being Term of the carrier of (DTConMSA X), st
( t' = p . i & the_sort_of t' = (the_arity_of o) . i ) )
assume A5: i in dom p ; :: thesis: ex t' being Term of the carrier of (DTConMSA X), st
( t' = p . i & the_sort_of t' = (the_arity_of o) . i )
then reconsider t = p . i as Term of the carrier of (DTConMSA Y), by MSATERM:22;
A6: t in rng p by A5, FUNCT_1:def 5;
Y variables_in t c= X

proof

let y be set ; :: according to PBOOLE:def 5 :: thesis: ( not y in the carrier of S or (Y variables_in t) . y c= X . y )
assume y in the carrier of S ; :: thesis: (Y variables_in t) . y c= X . y
then reconsider s = y as SortSymbol of ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Y variables_in t) . y or x in X . y )
assume x in (Y variables_in t) . y ; :: thesis: x in X . y
then A7: x in (Y variables_in ([o,the carrier of S] -tree p)) . s by A6, Th14;
(Y variables_in ([o,the carrier of S] -tree p)) . s c= X . s by A3, PBOOLE:def 5;
hence x in X . y by A7; :: thesis: verum

end;

then reconsider t' = t as Term of the carrier of (DTConMSA X), by A2, A6;
take t' = t'; :: thesis: ( t' = p . i & the_sort_of t' = (the_arity_of o) . i )
thus t' = p . i ; :: thesis: the_sort_of t' = (the_arity_of o) . i
the_sort_of t = (the_arity_of o) . i by A5, MSATERM:23;
hence the_sort_of t' = (the_arity_of o) . i by Th30; :: thesis: verum

end;

len p = len (the_arity_of o) by MSATERM:22;
then reconsider p = p as ArgumentSeq of Sym o,X by A4, MSATERM:24;
(Sym o,X) -tree p is Term of the carrier of (DTConMSA X), ;
hence [o,the carrier of S] -tree p is Term of the carrier of (DTConMSA X), by MSAFREE:def 11; :: thesis: verum

end;

assume variables_in t c= X ; :: thesis: t is Term of the carrier of (DTConMSA X),
then A8: Y variables_in t c= X by Th16;
A9: for s being SortSymbol of
for x being Element of Y . s holds S₁[ root-tree [x,s]]

proof

let s be SortSymbol of ; :: thesis: for x being Element of Y . s holds S₁[ root-tree [x,s]]
let x be Element of Y . s; :: thesis: S₁[ root-tree [x,s]]
assume Y variables_in (root-tree [x,s]) c= X ; :: thesis: root-tree [x,s] is Term of the carrier of (DTConMSA X),
then A10: (Y variables_in (root-tree [x,s])) . s c= X . s by PBOOLE:def 5;
(Y variables_in (root-tree [x,s])) . s = {x} by Th13;
then x in X . s by A10, ZFMISC_1:37;
hence root-tree [x,s] is Term of the carrier of (DTConMSA X), by MSATERM:4; :: thesis: verum

end;

for t being Term of the carrier of (DTConMSA Y), holds S₁[t] from MSATERM:sch 1(A9, A1);
hence t is Term of the carrier of (DTConMSA X), by A8; :: thesis: verum