let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in NonTerminals (DTConMSA X) ; :: thesis:
then x in { s where s is Symbol of (DTConMSA X) : ex n being FinSequence st s ==> n } by LANG1:def 3;
then consider s being Symbol of (DTConMSA X) such that
A4: ( s = x & ex n being FinSequence st s ==> n ) ;
consider n being FinSequence such that
A5: s ==> n by A4;
A6: [s,n] in the Rules of (DTConMSA X) by A5, LANG1:def 1;
reconsider s = s as Element of [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) ;
reconsider n = n as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by A6, ZFMISC_1:106;
[s,n] in REL X by A5, LANG1:def 1;
hence x in [:the carrier' of S,{the carrier of S}:] by A4, Def9; :: thesis:

end;

thus A7: Union (coprod X) c= Terminals (DTConMSA X) :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in Union (coprod X) ; :: thesis:
then x in [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) by XBOOLE_0:def 3;
then ( x in Terminals (DTConMSA X) or x in NonTerminals (DTConMSA X) ) by A2, XBOOLE_0:def 3;
hence x in Terminals (DTConMSA X) by A1, A3, A8, XBOOLE_0:3; :: thesis:

end;

assume A9: X is non-empty ; :: thesis:
thus NonTerminals (DTConMSA X) c= [:the carrier' of S,{the carrier of S}:] by A3; :: according to XBOOLE_0:def 10 :: thesis:
thus A10: [:the carrier' of S,{the carrier of S}:] c= NonTerminals (DTConMSA X) :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: x in [:the carrier' of S,{the carrier of S}:] ; :: thesis:
then consider o being OperSymbol of S, x2 being Element of {the carrier of S} such that
A12: x = [o,x2] by DOMAIN_1:9;
A13: the carrier of S = x2 by TARSKI:def 1;
then reconsider xa = [o,the carrier of S] as Element of the carrier of (DTConMSA X) by A11, A12, XBOOLE_0:def 3;
set O = the_arity_of o;
defpred S₁[ set , set ] means $2 in coprod ((the_arity_of o) . $1),X;
A14: 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 A15: ( (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 by A9;
then consider x being set such that
A16: 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 A15, A16, Def2; :: thesis:

end;

consider b being Function such that
A17: ( 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(A14);
reconsider b = b as FinSequence by A17, FINSEQ_1:def 2;
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
A18: ( c in dom b & b . c = a ) by FUNCT_1:def 5;
A19: a in coprod ((the_arity_of o) . c),X by A17, A18;
dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
then A20: ( (the_arity_of o) . c in rng (the_arity_of o) & rng (the_arity_of o) c= the carrier of S ) by A17, A18, 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 A20, FUNCT_1:def 5;
then coprod ((the_arity_of o) . c),X in rng (coprod X) by A20, Def3;
then a in union (rng (coprod X)) by A19, 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;
A21: len b = len (the_arity_of o) by A17, FINSEQ_1:def 3;

let c be set ; :: thesis:
assume A22: c in dom b ; :: thesis:
then A23: S₁[c,b . c] by A17;
dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
then A24: ( (the_arity_of o) . c in rng (the_arity_of o) & rng (the_arity_of o) c= the carrier of S ) by A17, A22, 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 A24, FUNCT_1:def 5;
then coprod ((the_arity_of o) . c),X in rng (coprod X) by A24, Def3;
then b . c in union (rng (coprod X)) by A23, 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 A17, A22; :: thesis:

end;

then [xa,b] in REL X by A21, Th5;
then xa ==> b by LANG1:def 1;
then xa in { t where t is Symbol of (DTConMSA X) : ex n being FinSequence st t ==> n } ;
hence x in NonTerminals (DTConMSA X) by A12, A13, LANG1:def 3; :: thesis:

end;

thus Terminals (DTConMSA X) c= Union (coprod X) :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A25: x in Terminals (DTConMSA X) ; :: thesis:
then A26: x in [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) by A2, XBOOLE_0:def 3;
not x in [:the carrier' of S,{the carrier of S}:] by A2, A10, A25, XBOOLE_0:3;
hence x in Union (coprod X) by A26, XBOOLE_0:def 3; :: thesis:

end;

thus Union (coprod X) c= Terminals (DTConMSA X) by A7; :: thesis: