set D = DTConMSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union ());
A1: Terminals () = Union () by Th6;
A2: NonTerminals () = [: the carrier' of S,{ the carrier of S}:] by Th6;
A3: Union () misses [: the carrier' of S,{ the carrier of S}:] by Th4;
for nt being Symbol of () st nt in NonTerminals () holds
ex p being FinSequence of TS () st nt ==> roots p
proof
let nt be Symbol of (); :: thesis: ( nt in NonTerminals () implies ex p being FinSequence of TS () st nt ==> roots p )
assume nt in NonTerminals () ; :: thesis: ex p being FinSequence of TS () st nt ==> roots p
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A4: nt = [o,x2] by ;
set O = the_arity_of o;
defpred S1[ object , object ] means X in coprod ((() . S),X);
A5: 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 A6: (the_arity_of o) . a in rng () by FUNCT_1:def 3;
A7: rng () c= the carrier of S by FINSEQ_1:def 4;
then consider x being object such that
A8: x in X . (() . a) by ;
take [x,(() . a)] ; :: thesis: S1[a,[x,(() . a)]]
thus S1[a,[x,(() . a)]] by A6, A7, A8, Def2; :: thesis: verum
end;
consider b being Function such that
A9: ( 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 ;
A10: 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 ()) )
A11: 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
A12: c in dom b and
A13: b . c = a by FUNCT_1:def 3;
dom () = Seg (len ()) by FINSEQ_1:def 3;
then A14: (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 A15: coprod ((() . c),X) in rng () by ;
a in coprod ((() . c),X) by A9, A12, A13;
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;
deffunc H1( object ) -> set = root-tree (b . S);
consider f being Function such that
A16: ( dom f = dom b & ( for x being object st x in dom b holds
f . x = H1(x) ) ) from reconsider f = f as FinSequence by ;
rng f c= TS ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in TS () )
A17: rng () c= the carrier of S by FINSEQ_1:def 4;
assume x in rng f ; :: thesis: x in TS ()
then consider y being object such that
A18: y in dom f and
A19: f . y = x by FUNCT_1:def 3;
dom () = Seg (len ()) by FINSEQ_1:def 3;
then A20: (the_arity_of o) . y in rng () by ;
dom () = the carrier of S by PARTFUN1:def 2;
then (coprod X) . (() . y) in rng () by ;
then A21: coprod ((() . y),X) in rng () by ;
b . y in rng b by ;
then reconsider a = b . y as Symbol of () by A10;
S1[y,b . y] by A9, A16, A18;
then b . y in union (rng ()) by ;
then A22: a in Terminals () by ;
x = root-tree (b . y) by ;
hence x in TS () by ; :: thesis: verum
end;
then reconsider f = f as FinSequence of TS () by FINSEQ_1:def 4;
A23: for x being object st x in dom b holds
() . x = b . x
proof
let x be object ; :: thesis: ( x in dom b implies () . x = b . x )
assume A24: x in dom b ; :: thesis: () . x = b . x
then reconsider i = x as Nat ;
( f . x = root-tree (b . x) & ex T being DecoratedTree st
( T = f . i & () . i = T . {} ) ) by ;
hence (roots f) . x = b . x by TREES_4:3; :: thesis: verum
end;
A25: 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 A26: 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 A27: (the_arity_of o) . c in rng () by ;
A28: 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 A29: 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;
( the carrier of S = x2 & len b = len () ) by ;
then [nt,b] in REL X by A4, A25, Th5;
then A30: nt ==> b by LANG1:def 1;
take f ; :: thesis: nt ==> roots f
dom () = dom f by TREES_3:def 18;
hence nt ==> roots f by ; :: thesis: verum
end;
hence ( DTConMSA X is with_terminals & DTConMSA X is with_nonterminals & DTConMSA X is with_useful_nonterminals ) by ; :: thesis: verum