let S be non void Signature; :: thesis:
let X be with_missing_variables ManySortedSet of ; :: thesis:
set V = X \/ (the carrier of S --> {0 });
set A = Free S,X;
set U = the Sorts of (Free S,X);
set G = DTConMSA X;
A1: the Sorts of (Free S,X) = S -Terms X,(X \/ (the carrier of S --> {0 })) by MSAFREE3:25;
A2: dom the Sorts of (Free S,X) = the carrier of S by PARTFUN1:def 4;
defpred S₁[ set ] means ( $1 in Union the Sorts of (Free S,X) implies $1 in TS (DTConMSA X) );
T1: for s being SortSymbol of S
for v being Element of (X \/ (the carrier of S --> {0 })) . s holds S₁[ root-tree [v,s]]

let s be SortSymbol of S; :: thesis:
let v be Element of (X \/ (the carrier of S --> {0 })) . s; :: thesis:
assume root-tree [v,s] in Union the Sorts of (Free S,X) ; :: thesis:
then consider s1 being set such that
Z1: ( s1 in dom the Sorts of (Free S,X) & root-tree [v,s] in the Sorts of (Free S,X) . s1 ) by CARD_5:10;
reconsider s1 = s1 as SortSymbol of S by Z1, PARTFUN1:def 4;
the Sorts of (Free S,X) . s1 = { t where t is Term of S,(X \/ (the carrier of S --> {0 })) : ( the_sort_of t = s1 & variables_in t c= X ) } by A1, MSAFREE3:def 6;
then consider t being Term of S,(X \/ (the carrier of S --> {0 })) such that
Z2: ( root-tree [v,s] = t & the_sort_of t = s1 & variables_in t c= X ) by Z1;
( s1 = s & (variables_in t) . s = {v} ) by Z2, MSAFREE3:11, MSATERM:14;
then {v} c= X . s by Z2, PBOOLE:def 5;
then v in X . s by ZFMISC_1:37;
then [v,s] in Terminals (DTConMSA X) by MSAFREE:7;
hence root-tree [v,s] in TS (DTConMSA X) by DTCONSTR:def 4; :: thesis:

end;

T2: for o being OperSymbol of S
for p being ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) st ( for t being Term of S,(X \/ (the carrier of S --> {0 })) st t in rng p holds
S₁[t] ) holds
S₁[[o,the carrier of S] -tree p]

let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })); :: thesis:
assume that
Y0: for t being Term of S,(X \/ (the carrier of S --> {0 })) st t in rng p holds
S₁[t] and
Y1: [o,the carrier of S] -tree p in Union the Sorts of (Free S,X) ; :: thesis:
consider s being set such that
Z1: ( s in dom the Sorts of (Free S,X) & [o,the carrier of S] -tree p in the Sorts of (Free S,X) . s ) by Y1, CARD_5:10;
reconsider s = s as SortSymbol of S by Z1, PARTFUN1:def 4;
the Sorts of (Free S,X) . s = { t where t is Term of S,(X \/ (the carrier of S --> {0 })) : ( the_sort_of t = s & variables_in t c= X ) } by A1, MSAFREE3:def 6;
then consider t being Term of S,(X \/ (the carrier of S --> {0 })) such that
Z2: ( [o,the carrier of S] -tree p = t & the_sort_of t = s & variables_in t c= X ) by Z1;
t . {} = [o,the carrier of S] by Z2, TREES_4:def 4;
then the_result_sort_of o = s by Z2, MSATERM:17;
then Y2: rng p c= Union the Sorts of (Free S,X) by A1, Z1, MSAFREE3:20;
rng p c= TS (DTConMSA X)

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume Y3: x in rng p ; :: thesis:
then x is Term of S,(X \/ (the carrier of S --> {0 })) by Y2, LemFT;
hence x in TS (DTConMSA X) by Y0, Y2, Y3; :: thesis:

end;

then reconsider q = p as FinSequence of TS (DTConMSA X) by FINSEQ_1:def 4;
NonTerminals (DTConMSA X) = [:the carrier' of S,{the carrier of S}:] by ThTNT;
then [o,the carrier of S] in NonTerminals (DTConMSA X) by ZFMISC_1:129;
then reconsider oo = [o,the carrier of S] as Symbol of (DTConMSA X) ;
Sym o,(X \/ (the carrier of S --> {0 })) ==> roots p by MSATERM:21;
then oo ==> roots q by LemArr;
hence [o,the carrier of S] -tree p in TS (DTConMSA X) by DTCONSTR:def 4; :: thesis:

end;

TT: for t being Term of S,(X \/ (the carrier of S --> {0 })) holds S₁[t] from MSATERM:sch 1(T1, T2);
A4: ( NonTerminals (DTConMSA X) = [:the carrier' of S,{the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) by ThTNT;
defpred S₂[ set ] means $1 in Union the Sorts of (Free S,X);
D1: for s being Symbol of (DTConMSA X) st s in Terminals (DTConMSA X) holds
S₂[ root-tree s]

let s be Symbol of (DTConMSA X); :: thesis:
assume s in Terminals (DTConMSA X) ; :: thesis:
then B1: ( s `2 in dom X & s `1 in X . (s `2 ) & s = [(s `1 ),(s `2 )] ) by A4, CARD_3:33;
B2: ( dom X = the carrier of S & dom the Sorts of (Free S,X) = the carrier of S ) by PARTFUN1:def 4;
then root-tree s in the Sorts of (Free S,X) . (s `2 ) by B1, MSAFREE3:5;
hence S₂[ root-tree s] by B1, B2, CARD_5:10; :: thesis:

end;

D2: for nt being Symbol of (DTConMSA X)
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S₂[t] ) holds
S₂[nt -tree ts]

let nt be Symbol of (DTConMSA X); :: thesis:
let ts be FinSequence of TS (DTConMSA X); :: thesis:
assume that
Z1: nt ==> roots ts and
Z2: for t being DecoratedTree of st t in rng ts holds
S₂[t] ; :: thesis:
nt in NonTerminals (DTConMSA X) by Z1;
then consider o, z being set such that
Z3: ( o in the carrier' of S & z in {the carrier of S} & nt = [o,z] ) by A4, ZFMISC_1:def 2;
reconsider o = o as OperSymbol of S by Z3;
Z5: rng ts c= Union the Sorts of (Free S,X)

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume Z6: a in rng ts ; :: thesis:
a is DecoratedTree of by Z6, TREES_3:def 6;
hence a in Union the Sorts of (Free S,X) by Z2, Z6; :: thesis:

end;

rng ts c= TS (DTConMSA (X \/ (the carrier of S --> {0 })))

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng ts ; :: thesis:
then ( a is Element of S -Terms (X \/ (the carrier of S --> {0 })) & S -Terms (X \/ (the carrier of S --> {0 })) = TS (DTConMSA (X \/ (the carrier of S --> {0 }))) ) by Z5, LemFT, MSATERM:def 1;
hence a in TS (DTConMSA (X \/ (the carrier of S --> {0 }))) ; :: thesis:

end;

then reconsider p = ts as FinSequence of TS (DTConMSA (X \/ (the carrier of S --> {0 }))) by FINSEQ_1:def 4;
reconsider q = p as FinSequence of S -Terms (X \/ (the carrier of S --> {0 })) by MSATERM:def 1;
Z4: z = the carrier of S by Z3, TARSKI:def 1;
then Sym o,(X \/ (the carrier of S --> {0 })) ==> roots p by Z1, Z3, LemArr;
then reconsider q = q as ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) by MSATERM:21;
set t = (Sym o,(X \/ (the carrier of S --> {0 }))) -tree q;
(Sym o,(X \/ (the carrier of S --> {0 }))) -tree q in the Sorts of (Free S,X) . (the_result_sort_of o) by A1, Z5, MSAFREE3:20;
hence S₂[nt -tree ts] by A2, Z3, Z4, CARD_5:10; :: thesis:

end;

DD: for t being DecoratedTree of st t in TS (DTConMSA X) holds
S₂[t] from DTCONSTR:sch 7(D1, D2);
thus Union the Sorts of (Free S,X) c= TS (DTConMSA X) :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume B1: x in Union the Sorts of (Free S,X) ; :: thesis:
then consider s being set such that
B2: ( s in dom the Sorts of (Free S,X) & x in the Sorts of (Free S,X) . s ) by CARD_5:10;
reconsider s = s as SortSymbol of S by B2, PARTFUN1:def 4;
x in the Sorts of (Free S,X) . s by B2;
then x is Term of S,(X \/ (the carrier of S --> {0 })) by A1, MSAFREE3:17;
hence x in TS (DTConMSA X) by B1, TT; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume C0: x in TS (DTConMSA X) ; :: thesis:
then reconsider TG = TS (DTConMSA X) as non empty Subset of (FinTrees the carrier of (DTConMSA X)) ;
x is Element of TG by C0;
hence x in Union the Sorts of (Free S,X) by DD; :: thesis: