consider f being Function of (TS G),((Terminals G) *) such that
A5: ( ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = H₇(t) ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = H₈(nt, roots ts,f * ts) ) ) from DTCONSTR:sch 8();
f . tsg is Element of (Terminals G) * by A1, FUNCT_2:5;
then reconsider IT = f . tsg as FinSequence of Terminals G ;
take IT ; :: thesis: ex f being Function of (TS G),((Terminals G) *) st
( IT = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) )
take f ; :: thesis: ( IT = f . tsg & ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) )
thus IT = f . tsg ; :: thesis: ( ( for t being Symbol of G st t in Terminals G holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) )

hereby :: thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts)

let t be Symbol of G; :: thesis: ( t in Terminals G implies f . (root-tree t) = <*t*> )
assume A6: t in Terminals G ; :: thesis: f . (root-tree t) = <*t*>
then f . (root-tree t) = s2t . t by A5;
hence f . (root-tree t) = <*t*> by A4, A6; :: thesis: verum

end;

thus for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) by A5; :: thesis: verum