let S be non void Signature; :: thesis:
let X be ManySortedSet of the carrier of S; :: thesis:
assume A1: X is with_missing_variables ; :: thesis:
set D = DTConMSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A2: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by MSAFREE:4;
A3: Terminals (DTConMSA X) misses NonTerminals (DTConMSA X) by DTCONSTR:8;
thus NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6; :: according to XBOOLE_0:def 10 :: thesis:
thus A4: [: the carrier' of S,{ the carrier of S}:] c= NonTerminals (DTConMSA X) :: thesis:

proof

let o, x2 be object ; :: according to RELAT_1:def 3 :: thesis:
assume A5: [o,x2] in [: the carrier' of S,{ the carrier of S}:] ; :: thesis:
then A6: x2 in { the carrier of S} by ZFMISC_1:87;
reconsider o = o as OperSymbol of S by A5, ZFMISC_1:87;
A7: the carrier of S = x2 by A6, TARSKI:def 1;
then reconsider xa = [o, the carrier of S] as Element of the carrier of (DTConMSA X) by A5, XBOOLE_0:def 3;
set O = the_arity_of o;
defpred S₁[ object , object ] means ( $2 in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) & ( X . ((the_arity_of o) . $1) <> {} implies $2 in coprod (((the_arity_of o) . $1),X) ) & ( X . ((the_arity_of o) . $1) = {} implies ex o being OperSymbol of S st
( $2 = [o, the carrier of S] & the_result_sort_of o = (the_arity_of o) . $1 ) ) );
A8: for a being object st a in Seg (len (the_arity_of o)) holds
ex b being object st S₁[a,b]

proof

let a be object ; :: thesis:
assume a in Seg (len (the_arity_of o)) ; :: thesis:
then A9: a in dom (the_arity_of o) by FINSEQ_1:def 3;
then A10: (the_arity_of o) . a in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider s = (the_arity_of o) . a as SortSymbol of S ;

per cases ;

suppose not X . ((the_arity_of o) . a) is empty ; :: thesis:

then consider x being object such that
A11: x in X . ((the_arity_of o) . a) by XBOOLE_0:def 1;
take y = [x,((the_arity_of o) . a)]; :: thesis:
A12: y in coprod (((the_arity_of o) . a),X) by A10, A11, MSAFREE:def 2;
A13: (the_arity_of o) . a in rng (the_arity_of o) by A9, FUNCT_1:def 3;
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . ((the_arity_of o) . a) in rng (coprod X) by A13, FUNCT_1:def 3;
then coprod (((the_arity_of o) . a),X) in rng (coprod X) by A13, MSAFREE:def 3;
then y in Union (coprod X) by A12, TARSKI:def 4;
hence S₁[a,y] by A10, A11, MSAFREE:def 2, XBOOLE_0:def 3; :: thesis:

end;

suppose A14: X . ((the_arity_of o) . a) = {} ; :: thesis:

then consider o being OperSymbol of S such that
A15: the_result_sort_of o = s by A1, Th114;
take y = [o, the carrier of S]; :: thesis:
the carrier of S in { the carrier of S} by TARSKI:def 1;
then y in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
hence S₁[a,y] by A14, A15, XBOOLE_0:def 3; :: thesis:

end;

end;

end;

consider b being Function such that
A16: ( 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(A8);
reconsider b = b as FinSequence by A16, FINSEQ_1:def 2;
rng b c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng b ; :: thesis:
then ex c being object st
( c in dom b & b . c = a ) by FUNCT_1:def 3;
hence a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by A16; :: 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;
A17: len b = len (the_arity_of o) by A16, FINSEQ_1:def 3;

now :: thesis:

let c be set ; :: thesis:
assume A18: c in dom b ; :: thesis:
then A19: S₁[c,b . c] by A16;
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) by A16, A18, FUNCT_1:def 3;
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A20, FUNCT_1:def 3;
then coprod (((the_arity_of o) . c),X) in rng (coprod X) by A20, MSAFREE:def 3;
then ( X . ((the_arity_of o) . c) <> {} implies b . c in Union (coprod X) ) by A19, TARSKI: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 A2, A19, XBOOLE_0:3, XTUPLE_0:1; :: thesis:
assume A21: b . c in Union (coprod X) ; :: thesis:

now :: thesis:

assume X . ((the_arity_of o) . c) = {} ; :: thesis:
then A22: ex o being OperSymbol of S st
( b . c = [o, the carrier of S] & the_result_sort_of o = (the_arity_of o) . c ) by A16, A18;
the carrier of S in { the carrier of S} by TARSKI:def 1;
then b . c in [: the carrier' of S,{ the carrier of S}:] by A22, ZFMISC_1:87;
hence contradiction by A2, A21, XBOOLE_0:3; :: thesis:

end;

hence b . c in coprod (((the_arity_of o) . c),X) by A16, A18; :: thesis:

end;

then [xa,b] in REL X by A17, MSAFREE:5;
then xa ==> b ;
hence x2 ast in NonTerminals (DTConMSA X) by A7; :: thesis:

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A23: x in Terminals (DTConMSA X) ; :: thesis:
then not x in [: the carrier' of S,{ the carrier of S}:] by A3, A4, XBOOLE_0:3;
hence x in Union (coprod X) by A23, XBOOLE_0:def 3; :: thesis:

end;

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