let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S holds

( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V5() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )

let X be ManySortedSet of the carrier of S; :: thesis: ( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V5() implies ( 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: the carrier of (DTConMSA X) = (Terminals (DTConMSA X)) \/ (NonTerminals (DTConMSA X)) by LANG1:1;

thus A2: NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] :: thesis: ( Union (coprod X) c= Terminals (DTConMSA X) & ( X is V5() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )

thus A7: Union (coprod X) c= Terminals (DTConMSA X) :: thesis: ( X is V5() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) )

thus NonTerminals (DTConMSA X) 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 (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)

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

( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V5() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )

let X be ManySortedSet of the carrier of S; :: thesis: ( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V5() implies ( 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: the carrier of (DTConMSA X) = (Terminals (DTConMSA X)) \/ (NonTerminals (DTConMSA X)) by LANG1:1;

thus A2: NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] :: thesis: ( Union (coprod X) c= Terminals (DTConMSA X) & ( X is V5() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )

proof

A6:
Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]
by Th4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NonTerminals (DTConMSA X) or x in [: the carrier' of S,{ the carrier of S}:] )

assume x in NonTerminals (DTConMSA X) ; :: thesis: x in [: the carrier' of S,{ the carrier of S}:]

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

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 (DTConMSA 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 REL X by A5, LANG1:def 1;

hence x in [: the carrier' of S,{ the carrier of S}:] by A3, Def7; :: thesis: verum

end;assume x in NonTerminals (DTConMSA X) ; :: thesis: x in [: the carrier' of S,{ the carrier of S}:]

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

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 (DTConMSA 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 REL X by A5, LANG1:def 1;

hence x in [: the carrier' of S,{ the carrier of S}:] by A3, Def7; :: thesis: verum

thus A7: Union (coprod X) c= Terminals (DTConMSA X) :: thesis: ( X is V5() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) )

proof

assume A9:
X is V5()
; :: thesis: ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (coprod X) or x in Terminals (DTConMSA X) )

assume A8: x in Union (coprod X) ; :: thesis: x in Terminals (DTConMSA X)

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 A1, XBOOLE_0:def 3;

hence x in Terminals (DTConMSA X) by A6, A2, A8, XBOOLE_0:3; :: thesis: verum

end;assume A8: x in Union (coprod X) ; :: thesis: x in Terminals (DTConMSA X)

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 A1, XBOOLE_0:def 3;

hence x in Terminals (DTConMSA X) by A6, A2, A8, XBOOLE_0:3; :: thesis: verum

thus NonTerminals (DTConMSA X) 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 (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

A29:
Terminals (DTConMSA X) misses NonTerminals (DTConMSA X)
by DTCONSTR:8;
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 (DTConMSA X) )

assume A11: x in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: x in NonTerminals (DTConMSA X)

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 S_{1}[ object , object ] means $2 in coprod (((the_arity_of o) . $1),X);

A13: for a being object st a in Seg (len (the_arity_of o)) holds

ex b being object st S_{1}[a,b]

A17: ( dom b = Seg (len (the_arity_of o)) & ( for a being object st a in Seg (len (the_arity_of o)) holds

S_{1}[a,b . a] ) )
from CLASSES1:sch 1(A13);

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

reconsider b = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def 11;

then reconsider xa = [o, the carrier of S] as Element of the carrier of (DTConMSA X) by A11, A12, XBOOLE_0:def 3;

len b = len (the_arity_of o) by A17, FINSEQ_1:def 3;

then [xa,b] in REL X by A23, 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, A28, LANG1:def 3; :: thesis: verum

end;assume A11: x in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: x in NonTerminals (DTConMSA X)

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 S

A13: for a being object st a in Seg (len (the_arity_of o)) holds

ex b being object st S

proof

consider b being Function such that
let a be object ; :: thesis: ( a in Seg (len (the_arity_of o)) implies ex b being object st S_{1}[a,b] )

assume a in Seg (len (the_arity_of o)) ; :: thesis: ex b being object st S_{1}[a,b]

then a in dom (the_arity_of o) by FINSEQ_1:def 3;

then A14: (the_arity_of o) . a in rng (the_arity_of o) by FUNCT_1:def 3;

A15: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

then consider x being object such that

A16: x in X . ((the_arity_of o) . a) by A9, A14, XBOOLE_0:def 1;

take [x,((the_arity_of o) . a)] ; :: thesis: S_{1}[a,[x,((the_arity_of o) . a)]]

thus S_{1}[a,[x,((the_arity_of o) . a)]]
by A14, A15, A16, Def2; :: thesis: verum

end;assume a in Seg (len (the_arity_of o)) ; :: thesis: ex b being object st S

then a in dom (the_arity_of o) by FINSEQ_1:def 3;

then A14: (the_arity_of o) . a in rng (the_arity_of o) by FUNCT_1:def 3;

A15: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

then consider x being object such that

A16: x in X . ((the_arity_of o) . a) by A9, A14, XBOOLE_0:def 1;

take [x,((the_arity_of o) . a)] ; :: thesis: S

thus S

A17: ( dom b = Seg (len (the_arity_of o)) & ( for a being object st a in Seg (len (the_arity_of o)) holds

S

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

then reconsider b = b as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def 4;
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 (coprod X)) )

A18: rng (the_arity_of o) 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 (coprod X))

then consider c being object such that

A19: c in dom b and

A20: b . c = a by FUNCT_1:def 3;

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A21: (the_arity_of o) . c in rng (the_arity_of o) by A17, A19, 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 A21, A18, FUNCT_1:def 3;

then A22: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A21, A18, Def3;

a in coprod (((the_arity_of o) . c),X) by A17, A19, A20;

then a in union (rng (coprod X)) by A22, 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: verum

end;A18: rng (the_arity_of o) 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 (coprod X))

then consider c being object such that

A19: c in dom b and

A20: b . c = a by FUNCT_1:def 3;

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A21: (the_arity_of o) . c in rng (the_arity_of o) by A17, A19, 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 A21, A18, FUNCT_1:def 3;

then A22: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A21, A18, Def3;

a in coprod (((the_arity_of o) . c),X) by A17, A19, A20;

then a in union (rng (coprod X)) by A22, 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: verum

reconsider b = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * 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 = (the_arity_of o) . c ) & ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) ) )

A28:
the carrier of S = x2
by TARSKI:def 1;( ( 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) ) )

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

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A25: (the_arity_of o) . c in rng (the_arity_of o) by A17, A24, FUNCT_1:def 3;

A26: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

dom (coprod X) = the carrier of S by PARTFUN1:def 2;

then (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A25, A26, FUNCT_1:def 3;

then A27: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A25, A26, Def3;

S_{1}[c,b . c]
by A17, A24;

then b . c in union (rng (coprod X)) by A27, 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: ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) )

assume b . c in Union (coprod X) ; :: thesis: b . c in coprod (((the_arity_of o) . c),X)

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

end;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 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 = (the_arity_of o) . c ) & ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) ) )

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A25: (the_arity_of o) . c in rng (the_arity_of o) by A17, A24, FUNCT_1:def 3;

A26: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

dom (coprod X) = the carrier of S by PARTFUN1:def 2;

then (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A25, A26, FUNCT_1:def 3;

then A27: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A25, A26, Def3;

S

then b . c in union (rng (coprod X)) by A27, 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: ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) )

assume b . c in Union (coprod X) ; :: thesis: b . c in coprod (((the_arity_of o) . c),X)

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

then reconsider xa = [o, the carrier of S] as Element of the carrier of (DTConMSA X) by A11, A12, XBOOLE_0:def 3;

len b = len (the_arity_of o) by A17, FINSEQ_1:def 3;

then [xa,b] in REL X by A23, 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, A28, LANG1:def 3; :: thesis: verum

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

proof

thus
Union (coprod X) c= Terminals (DTConMSA X)
by A7; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Terminals (DTConMSA X) or x in Union (coprod X) )

assume x in Terminals (DTConMSA X) ; :: thesis: x in Union (coprod X)

then ( x in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) & not x in [: the carrier' of S,{ the carrier of S}:] ) by A1, A29, A10, XBOOLE_0:3, XBOOLE_0:def 3;

hence x in Union (coprod X) by XBOOLE_0:def 3; :: thesis: verum

end;assume x in Terminals (DTConMSA X) ; :: thesis: x in Union (coprod X)

then ( x in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) & not x in [: the carrier' of S,{ the carrier of S}:] ) by A1, A29, A10, XBOOLE_0:3, XBOOLE_0:def 3;

hence x in Union (coprod X) by XBOOLE_0:def 3; :: thesis: verum