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
f1 = f2 from DTCONSTR:sch 9(A13, A15);
hence it1 = it2 by A7, A10; :: thesis: verum