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

proof

let o, x2 be set ; :: according to RELAT_1:def 3 :: thesis: ( not x2 ast in [:the carrier' of S,{the carrier of S}:] or x2 ast in NonTerminals (DTConMSA X) )
assume A11: [o,x2] in [:the carrier' of S,{the carrier of S}:] ; :: thesis: x2 ast in NonTerminals (DTConMSA X)
then A12: ( o in the carrier' of S & x2 in {the carrier of S} ) by ZFMISC_1:106;
then reconsider o = o as OperSymbol of S ;
A13: the carrier of S = x2 by A12, TARSKI:def 1;
then reconsider xa = [o,the carrier of S] as Element of the carrier of (DTConMSA X) by A11, XBOOLE_0:def 3;
set O = the_arity_of o;
defpred S₁[ set , set ] 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 ) ) );
A14: for a being set st a in Seg (len (the_arity_of o)) holds
ex b being set st S₁[a,b]

proof

let a be set ; :: thesis: ( a in Seg (len (the_arity_of o)) implies ex b being set st S₁[a,b] )
assume a in Seg (len (the_arity_of o)) ; :: thesis: ex b being set st S₁[a,b]
then A18: 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 FUNCT_1:def 5;
then reconsider s = (the_arity_of o) . a as SortSymbol of S ;

per cases ( not X . ((the_arity_of o) . a) is empty or X . ((the_arity_of o) . a) = {} ) ;

suppose not X . ((the_arity_of o) . a) is empty ; :: thesis: ex b being set st S₁[a,b]

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: S₁[a,y]
A19: y in coprod ((the_arity_of o) . a),X by A15, A16, MSAFREE:def 2;
A20: ( (the_arity_of o) . a in rng (the_arity_of o) & rng (the_arity_of o) c= the carrier of S ) by A18, FUNCT_1:def 5;
dom (coprod X) = the carrier of S by PARTFUN1:def 4;
then (coprod X) . ((the_arity_of o) . a) in rng (coprod X) by A20, FUNCT_1:def 5;
then coprod ((the_arity_of o) . a),X in rng (coprod X) by A20, MSAFREE:def 3;
then y in Union (coprod X) by A19, TARSKI:def 4;
hence S₁[a,y] by A15, A16, MSAFREE:def 2, XBOOLE_0:def 3; :: thesis: verum

end;

suppose AA: X . ((the_arity_of o) . a) = {} ; :: thesis: ex b being set st S₁[a,b]

then consider o being OperSymbol of S such that
A3: the_result_sort_of o = s by A0, LemMV;
take y = [o,the carrier of S]; :: thesis: S₁[a,y]
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:106;
hence S₁[a,y] by AA, A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;

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))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng b or a in [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) )
assume a in rng b ; :: thesis: a in [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))
then ex c being set st
( c in dom b & b . c = a ) by FUNCT_1:def 5;
hence a in [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) by A17; :: thesis: verum

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;

now

let c be set ; :: thesis: ( c in dom b implies ( ( 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 ) & ( b . c in Union (coprod X) implies b . c in coprod ((the_arity_of o) . c),X ) ) )
assume A22: c in dom b ; :: thesis: ( ( 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 ) & ( b . c in Union (coprod X) implies b . c in coprod ((the_arity_of o) . c),X ) )
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, 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, MSAFREE:def 3;
then AB: ( X . ((the_arity_of o) . c) <> {} implies b . c in Union (coprod X) ) by A23, TARSKI:def 4;
thus ( 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 A23, A1, AB, XBOOLE_0:3, ZFMISC_1:33; :: thesis: ( b . c in Union (coprod X) implies b . c in coprod ((the_arity_of o) . c),X )
assume B1: b . c in Union (coprod X) ; :: thesis: b . c in coprod ((the_arity_of o) . c),X

now

assume X . ((the_arity_of o) . c) = {} ; :: thesis: contradiction
then consider o being OperSymbol of S such that
B2: ( b . c = [o,the carrier of S] & the_result_sort_of o = (the_arity_of o) . c ) by A17, A22;
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 B2, ZFMISC_1:106;
hence contradiction by B1, A1, XBOOLE_0:3; :: thesis: verum

end;

hence b . c in coprod ((the_arity_of o) . c),X by A17, A22; :: thesis: verum

end;

then [xa,b] in REL X by A21, MSAFREE:5;
then xa ==> b by LANG1:def 1;
hence x2 ast in NonTerminals (DTConMSA X) by A13; :: thesis: verum

end;

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

proof

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

end;

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