let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S holds
( NonTerminals () c= [: the carrier' of S,{ the carrier of S}:] & Union () c= Terminals () & ( X is V5() implies ( NonTerminals () = [: the carrier' of S,{ the carrier of S}:] & Terminals () = Union () ) ) )

let X be ManySortedSet of the carrier of S; :: thesis: ( NonTerminals () c= [: the carrier' of S,{ the carrier of S}:] & Union () c= Terminals () & ( X is V5() implies ( NonTerminals () = [: the carrier' of S,{ the carrier of S}:] & Terminals () = Union () ) ) )
set D = DTConMSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union ());
A1: the carrier of () = () \/ () by LANG1:1;
thus A2: NonTerminals () c= [: the carrier' of S,{ the carrier of S}:] :: thesis: ( Union () c= Terminals () & ( X is V5() implies ( NonTerminals () = [: the carrier' of S,{ the carrier of S}:] & Terminals () = Union () ) ) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NonTerminals () or x in [: the carrier' of S,{ the carrier of S}:] )
assume x in NonTerminals () ; :: thesis: x in [: the carrier' of S,{ the carrier of S}:]
then x in { s where s is Symbol of () : ex n being FinSequence st s ==> n } by LANG1:def 3;
then consider s being Symbol of () 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 () by ;
then reconsider n = n as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * by ZFMISC_1:87;
reconsider s = s as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) ;
[s,n] in REL X by ;
hence x in [: the carrier' of S,{ the carrier of S}:] by ; :: thesis: verum
end;
A6: Union () misses [: the carrier' of S,{ the carrier of S}:] by Th4;
thus A7: Union () c= Terminals () :: thesis: ( X is V5() implies ( NonTerminals () = [: the carrier' of S,{ the carrier of S}:] & Terminals () = Union () ) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union () or x in Terminals () )
assume A8: x in Union () ; :: thesis: x in Terminals ()
then x in [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) by XBOOLE_0:def 3;
then ( x in Terminals () or x in NonTerminals () ) by ;
hence x in Terminals () by ; :: thesis: verum
end;
assume A9: X is V5() ; :: thesis: ( NonTerminals () = [: the carrier' of S,{ the carrier of S}:] & Terminals () = Union () )
thus NonTerminals () c= [: the carrier' of S,{ the carrier of S}:] by A2; :: according to XBOOLE_0:def 10 :: thesis: ( [: the carrier' of S,{ the carrier of S}:] c= NonTerminals () & Terminals () = Union () )
thus A10: [: the carrier' of S,{ the carrier of S}:] c= NonTerminals () :: thesis: Terminals () = Union ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [: the carrier' of S,{ the carrier of S}:] or x in NonTerminals () )
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:1;
set O = the_arity_of o;
defpred S1[ object , object ] means \$2 in coprod ((() . \$1),X);
A13: for a being object st a in Seg (len ()) holds
ex b being object st S1[a,b]
proof
let a be object ; :: thesis: ( a in Seg (len ()) implies ex b being object st S1[a,b] )
assume a in Seg (len ()) ; :: thesis: ex b being object st S1[a,b]
then a in dom () by FINSEQ_1:def 3;
then A14: (the_arity_of o) . a in rng () by FUNCT_1:def 3;
A15: rng () c= the carrier of S by FINSEQ_1:def 4;
then consider x being object such that
A16: x in X . (() . a) by ;
take [x,(() . a)] ; :: thesis: S1[a,[x,(() . a)]]
thus S1[a,[x,(() . a)]] by ; :: thesis: verum
end;
consider b being Function such that
A17: ( dom b = Seg (len ()) & ( for a being object st a in Seg (len ()) holds
S1[a,b . a] ) ) from reconsider b = b as FinSequence by ;
rng b c= [: the carrier' of S,{ the carrier of S}:] \/ (Union ())
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng b or a in [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) )
A18: rng () c= the carrier of S by FINSEQ_1:def 4;
assume a in rng b ; :: thesis: a in [: the carrier' of S,{ the carrier of S}:] \/ (Union ())
then consider c being object such that
A19: c in dom b and
A20: b . c = a by FUNCT_1:def 3;
dom () = Seg (len ()) by FINSEQ_1:def 3;
then A21: (the_arity_of o) . c in rng () by ;
dom () = the carrier of S by PARTFUN1:def 2;
then (coprod X) . (() . c) in rng () by ;
then A22: coprod ((() . c),X) in rng () by ;
a in coprod ((() . c),X) by ;
then a in union (rng ()) by ;
then a in Union () by CARD_3:def 4;
hence a in [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) by XBOOLE_0:def 3; :: thesis: verum
end;
then reconsider b = b as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) by FINSEQ_1:def 4;
reconsider b = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * by FINSEQ_1:def 11;
A23: now :: thesis: for c being set st c in dom b holds
( ( 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 = () . c ) & ( b . c in Union () implies b . c in coprod ((() . c),X) ) )
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 = () . c ) & ( b . c in Union () implies b . c in coprod ((() . c),X) ) ) )

assume A24: 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 = () . c ) & ( b . c in Union () implies b . c in coprod ((() . c),X) ) )

dom () = Seg (len ()) by FINSEQ_1:def 3;
then A25: (the_arity_of o) . c in rng () by ;
A26: rng () c= the carrier of S by FINSEQ_1:def 4;
dom () = the carrier of S by PARTFUN1:def 2;
then (coprod X) . (() . c) in rng () by ;
then A27: coprod ((() . c),X) in rng () by ;
S1[c,b . c] by ;
then b . c in union (rng ()) by ;
then b . c in Union () 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 = () . c ) by ; :: thesis: ( b . c in Union () implies b . c in coprod ((() . c),X) )
assume b . c in Union () ; :: thesis: b . c in coprod ((() . c),X)
thus b . c in coprod ((() . c),X) by ; :: thesis: verum
end;
A28: the carrier of S = x2 by TARSKI:def 1;
then reconsider xa = [o, the carrier of S] as Element of the carrier of () by ;
len b = len () by ;
then [xa,b] in REL X by ;
then xa ==> b by LANG1:def 1;
then xa in { t where t is Symbol of () : ex n being FinSequence st t ==> n } ;
hence x in NonTerminals () by ; :: thesis: verum
end;
A29: Terminals () misses NonTerminals () by DTCONSTR:8;
thus Terminals () c= Union () :: according to XBOOLE_0:def 10 :: thesis: Union () c= Terminals ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Terminals () or x in Union () )
assume x in Terminals () ; :: thesis: x in Union ()
then ( x in [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) & not x in [: the carrier' of S,{ the carrier of S}:] ) by ;
hence x in Union () by XBOOLE_0:def 3; :: thesis: verum
end;
thus Union () c= Terminals () by A7; :: thesis: verum