let G be non empty with_terminals with_nonterminals DTConstrStr ; :: thesis:
defpred S₂[ DecoratedTree of the carrier of G] means for nt being NonTerminal of G st $1 . {} = nt holds
ex ts being FinSequence of TS G st
( $1 = nt -tree ts & nt ==> roots ts );

A1: now :: thesis:

let s be Symbol of G; :: thesis:
assume A2: s in Terminals G ; :: thesis:
thus S₂[ root-tree s] :: thesis:

proof

let nt be NonTerminal of G; :: thesis:
assume (root-tree s) . {} = nt ; :: thesis:
then A3: s = nt by TREES_4:3;
Terminals G = { t where t is Symbol of G : for tnt being FinSequence holds not t ==> tnt } by LANG1:def 2;
then A4: ex t being Symbol of G st
( s = t & ( for tnt being FinSequence holds not t ==> tnt ) ) by A2;
A5: nt in NonTerminals G ;
NonTerminals G = { t where t is Symbol of G : ex tnt being FinSequence st t ==> tnt } by LANG1:def 3;
then ex t being Symbol of G st
( nt = t & ex tnt being FinSequence st t ==> tnt ) by A5;
hence ex ts being FinSequence of TS G st
( root-tree s = nt -tree ts & nt ==> roots ts ) by A3, A4; :: thesis:

end;

end;

A6: now :: thesis:

let nnt be Symbol of G; :: thesis:
let tts be FinSequence of TS G; :: thesis:
assume that
A7: nnt ==> roots tts and
for t being DecoratedTree of the carrier of G st t in rng tts holds
S₂[t] ; :: thesis:
thus S₂[nnt -tree tts] :: thesis:

proof

let nt be NonTerminal of G; :: thesis:
assume A8: (nnt -tree tts) . {} = nt ; :: thesis:
take ts = tts; :: thesis:
thus ( nnt -tree tts = nt -tree ts & nt ==> roots ts ) by A7, A8, TREES_4:def 4; :: thesis:

end;

end;

A9: for t being DecoratedTree of the carrier of G st t in TS G holds
S₂[t] from DTCONSTR:sch 7(A1, A6);
let tsg be Element of TS G; :: thesis:
let nt be NonTerminal of G; :: thesis:
assume tsg . {} = nt ; :: thesis:
hence ex ts being FinSequence of TS G st
( tsg = nt -tree ts & nt ==> roots ts ) by A9; :: thesis: