let nt be Symbol of (DTConMSA X); :: thesis:
assume nt in NonTerminals (DTConMSA X) ; :: thesis:
then consider o being OperSymbol of S, x2 being Element of {the carrier of S} such that
A3: nt = [o,x2] by A2, DOMAIN_1:9;
A4: the carrier of S = x2 by TARSKI:def 1;
set O = the_arity_of o;
defpred S₁[ set , set ] means X in coprod ((the_arity_of o) . S),X;
A5: for a being set st a in Seg (len (the_arity_of o)) holds
ex b being set st S₁[a,b]

let a be set ; :: thesis:
assume a in Seg (len (the_arity_of o)) ; :: thesis:
then a in dom (the_arity_of o) by FINSEQ_1:def 3;
then A6: ( (the_arity_of o) . a in rng (the_arity_of o) & rng (the_arity_of o) c= the carrier of S ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then not X . ((the_arity_of o) . a) is empty ;
then consider x being set such that
A7: x in X . ((the_arity_of o) . a) by XBOOLE_0:def 1;
take y = [x,((the_arity_of o) . a)]; :: thesis:
thus S₁[a,y] by A6, A7, Def2; :: thesis:

end;

consider b being Function such that
A8: ( dom b = Seg (len (the_arity_of o)) & ( for a being set st a in Seg (len (the_arity_of o)) holds
S₁[a,b . a] ) ) from CLASSES1:sch 1(A5);
reconsider b = b as FinSequence by A8, FINSEQ_1:def 2;
A9: rng b c= [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng b ; :: thesis:
then consider c being set such that
A10: ( c in dom b & b . c = a ) by FUNCT_1:def 5;
A11: a in coprod ((the_arity_of o) . c),X by A8, A10;
dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
then A12: ( (the_arity_of o) . c in rng (the_arity_of o) & rng (the_arity_of o) c= the carrier of S ) by A8, A10, FINSEQ_1:def 4, FUNCT_1:def 5;
dom (coprod X) = the carrier of S by PARTFUN1:def 4;
then (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A12, FUNCT_1:def 5;
then coprod ((the_arity_of o) . c),X in rng (coprod X) by A12, Def3;
then a in union (rng (coprod X)) by A11, TARSKI:def 4;
then a in Union (coprod X) by CARD_3:def 4;
hence a in [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) by XBOOLE_0:def 3; :: thesis:

end;

then reconsider b = b as FinSequence of [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def 4;
reconsider b = b as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def 11;
A13: len b = len (the_arity_of o) by A8, FINSEQ_1:def 3;

let c be set ; :: thesis:
assume A14: c in dom b ; :: thesis:
then A15: S₁[c,b . c] by A8;
dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
then A16: ( (the_arity_of o) . c in rng (the_arity_of o) & rng (the_arity_of o) c= the carrier of S ) by A8, A14, FINSEQ_1:def 4, FUNCT_1:def 5;
dom (coprod X) = the carrier of S by PARTFUN1:def 4;
then (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A16, FUNCT_1:def 5;
then coprod ((the_arity_of o) . c),X in rng (coprod X) by A16, Def3;
then b . c in union (rng (coprod X)) by A15, TARSKI:def 4;
then b . c in Union (coprod X) by CARD_3:def 4;
hence ( b . c in [:the carrier' of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b . c holds
the_result_sort_of o1 = (the_arity_of o) . c ) by A1, XBOOLE_0:3; :: thesis:
assume b . c in Union (coprod X) ; :: thesis:
thus b . c in coprod ((the_arity_of o) . c),X by A8, A14; :: thesis:

end;

then [nt,b] in REL X by A3, A4, A13, Th5;
then A17: nt ==> b by LANG1:def 1;
deffunc H₁( set ) -> set = root-tree (b . S);
consider f being Function such that
A18: ( dom f = dom b & ( for x being set st x in dom b holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
reconsider f = f as FinSequence by A8, A18, FINSEQ_1:def 2;
rng f c= TS (DTConMSA X)

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being set such that
A19: ( y in dom f & f . y = x ) by FUNCT_1:def 5;
A20: x = root-tree (b . y) by A18, A19;
b . y in rng b by A18, A19, FUNCT_1:def 5;
then reconsider a = b . y as Symbol of (DTConMSA X) by A9;
A21: S₁[y,b . y] by A8, A18, A19;
dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
then A22: ( (the_arity_of o) . y in rng (the_arity_of o) & rng (the_arity_of o) c= the carrier of S ) by A8, A18, A19, FINSEQ_1:def 4, FUNCT_1:def 5;
dom (coprod X) = the carrier of S by PARTFUN1:def 4;
then (coprod X) . ((the_arity_of o) . y) in rng (coprod X) by A22, FUNCT_1:def 5;
then coprod ((the_arity_of o) . y),X in rng (coprod X) by A22, Def3;
then b . y in union (rng (coprod X)) by A21, TARSKI:def 4;
then a in Terminals (DTConMSA X) by A2, CARD_3:def 4;
hence x in TS (DTConMSA X) by A20, DTCONSTR:def 4; :: thesis:

end;

then reconsider f = f as FinSequence of TS (DTConMSA X) by FINSEQ_1:def 4;
take f ; :: thesis:
A23: dom (roots f) = dom f by TREES_3:def 18;
for x being set st x in dom b holds
(roots f) . x = b . x

let x be set ; :: thesis:
assume A24: x in dom b ; :: thesis:
then A25: f . x = root-tree (b . x) by A18;
reconsider i = x as Nat by A24;
consider T being DecoratedTree such that
A26: ( T = f . i & (roots f) . i = T . {} ) by A18, A24, TREES_3:def 18;
thus (roots f) . x = b . x by A25, A26, TREES_4:3; :: thesis:

end;

hence nt ==> roots f by A17, A18, A23, FUNCT_1:9; :: thesis:

end;

hence ( DTConMSA X is with_terminals & DTConMSA X is with_nonterminals & DTConMSA X is with_useful_nonterminals ) by A2, DTCONSTR:def 6, DTCONSTR:def 7, DTCONSTR:def 8; :: thesis: