let it1, it2 be FinSequence of Terminals G; :: thesis: ( ex f being Function of (TS G),((Terminals G) *) st
( it1 = 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) ) ) & ex f being Function of (TS G),((Terminals G) *) st
( it2 = 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) ) ) implies it1 = it2 )
given f1 being Function of (TS G),((Terminals G) *) such that A7: it1 = f1 . tsg and
A8: for t being Symbol of G st t in Terminals G holds
f1 . (root-tree t) = <*t*> and
A9: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = FlattenSeq (f1 * ts) ; :: thesis: ( for f being Function of (TS G),((Terminals G) *) holds
( not it2 = f . tsg or ex t being Symbol of G st
( t in Terminals G & not f . (root-tree t) = <*t*> ) or ex nt being Symbol of G ex ts being FinSequence of TS G st
( nt ==> roots ts & not f . (nt -tree ts) = FlattenSeq (f * ts) ) ) or it1 = it2 )
given f2 being Function of (TS G),((Terminals G) *) such that A10: it2 = f2 . tsg and
A11: for t being Symbol of G st t in Terminals G holds
f2 . (root-tree t) = <*t*> and
A12: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = FlattenSeq (f2 * ts) ; :: thesis: it1 = it2

A13: now :: thesis: ( ( for t being Symbol of G st t in Terminals G holds
f1 . (root-tree t) = H₇(t) ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H₈(nt, roots ts,f1 * ts) ) )

hereby :: thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H₈(nt, roots ts,f1 * ts)

let t be Symbol of G; :: thesis: ( t in Terminals G implies f1 . (root-tree t) = H₇(t) )
assume A14: t in Terminals G ; :: thesis: f1 . (root-tree t) = H₇(t)
hence f1 . (root-tree t) = <*t*> by A8
.= H₇(t) by A4, A14 ;
:: thesis: verum

end;

thus for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H₈(nt, roots ts,f1 * ts) by A9; :: thesis: verum

end;

A15: now :: thesis: ( ( for t being Symbol of G st t in Terminals G holds
f2 . (root-tree t) = H₇(t) ) & ( for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H₈(nt, roots ts,f2 * ts) ) )

hereby :: thesis: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H₈(nt, roots ts,f2 * ts)

let t be Symbol of G; :: thesis: ( t in Terminals G implies f2 . (root-tree t) = H₇(t) )
assume A16: t in Terminals G ; :: thesis: f2 . (root-tree t) = H₇(t)
hence f2 . (root-tree t) = <*t*> by A11
.= H₇(t) by A4, A16 ;
:: thesis: verum

end;

thus for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H₈(nt, roots ts,f2 * ts) by A12; :: thesis: verum

end;

f1 = f2 from DTCONSTR:sch 9(A13, A15);
hence it1 = it2 by A7, A10; :: thesis: verum