let S be OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
set D = DTConOSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A1: the carrier of (DTConOSA X) = (Terminals (DTConOSA X)) \/ (NonTerminals (DTConOSA X)) by LANG1:1;
thus A2: NonTerminals (DTConOSA X) c= [: the carrier' of S,{ the carrier of S}:] :: according to XBOOLE_0:def 10 :: thesis:

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

end;

A6: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by MSAFREE:4;
thus A7: [: the carrier' of S,{ the carrier of S}:] c= NonTerminals (DTConOSA X) :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in [: the carrier' of S,{ the carrier of S}:] ; :: thesis:
then consider o being Element of the carrier' of S, x2 being Element of { the carrier of S} such that
A9: x = [o,x2] by DOMAIN_1:1;
set O = the_arity_of o;
defpred S₁[ object , object ] means ex i being Element of S st
( i <= (the_arity_of o) /. $1 & $2 in coprod (i,X) );
A10: for a being object st a in Seg (len (the_arity_of o)) holds
ex b being object st S₁[a,b]

let a be object ; :: thesis:
assume a in Seg (len (the_arity_of o)) ; :: thesis:
then A11: a in dom (the_arity_of o) by FINSEQ_1:def 3;
then A12: (the_arity_of o) . a in rng (the_arity_of o) by FUNCT_1:def 3;
A13: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;
then consider x being object such that
A14: x in X . ((the_arity_of o) . a) by A12, XBOOLE_0:def 1;
take y = [x,((the_arity_of o) . a)]; :: thesis:
take (the_arity_of o) /. a ; :: thesis:
y in coprod (((the_arity_of o) . a),X) by A12, A13, A14, MSAFREE:def 2;
hence ( (the_arity_of o) /. a <= (the_arity_of o) /. a & y in coprod (((the_arity_of o) /. a),X) ) by A11, PARTFUN1:def 6; :: thesis:

end;

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

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng b ; :: thesis:
then consider c being object such that
A16: c in dom b and
A17: b . c = a by FUNCT_1:def 3;
consider i being Element of S such that
i <= (the_arity_of o) /. c and
A18: a in coprod (i,X) by A15, A16, A17;
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . i in rng (coprod X) by FUNCT_1:def 3;
then coprod (i,X) in rng (coprod X) by MSAFREE:def 3;
then a in union (rng (coprod X)) by A18, 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;

A19: now :: thesis:

let c be set ; :: thesis:
assume c in dom b ; :: thesis:
then consider i being Element of S such that
A20: i <= (the_arity_of o) /. c and
A21: b . c in coprod (i,X) by A15;
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . i in rng (coprod X) by FUNCT_1:def 3;
then coprod (i,X) in rng (coprod X) by MSAFREE:def 3;
then b . c in union (rng (coprod X)) by A21, 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 A6, XBOOLE_0:3; :: thesis:
assume b . c in Union (coprod X) ; :: thesis:
thus ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) by A20, A21; :: thesis:

end;

A22: the carrier of S = x2 by TARSKI:def 1;
then reconsider xa = [o, the carrier of S] as Element of the carrier of (DTConOSA X) by A8, A9, XBOOLE_0:def 3;
len b = len (the_arity_of o) by A15, FINSEQ_1:def 3;
then [xa,b] in OSREL X by A19, Th2;
then xa ==> b by LANG1:def 1;
then xa in { t where t is Symbol of (DTConOSA X) : ex n being FinSequence st t ==> n } ;
hence x in NonTerminals (DTConOSA X) by A9, A22, LANG1:def 3; :: thesis:

end;

A23: Terminals (DTConOSA X) misses NonTerminals (DTConOSA X) by DTCONSTR:8;
thus Terminals (DTConOSA X) c= Union (coprod X) :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A24: x in Terminals (DTConOSA X) ; :: thesis:
then A25: x in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by A1, XBOOLE_0:def 3;
not x in [: the carrier' of S,{ the carrier of S}:] by A23, A7, A24, XBOOLE_0:3;
hence x in Union (coprod X) by A25, XBOOLE_0:def 3; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: 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 (DTConOSA X) or x in NonTerminals (DTConOSA X) ) by A1, XBOOLE_0:def 3;
hence x in Terminals (DTConOSA X) by A6, A2, A26, XBOOLE_0:3; :: thesis: