consider f being Function of (TS G),( the carrier of G *) such that
A30: ( ( 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 the carrier of G * by A1, FUNCT_2:5;
then reconsider IT = f . tsg as FinSequence of the carrier of G ;
take IT ; :: thesis: ex f being Function of (TS G),( the carrier of 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
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) )
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
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) )
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
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> ) )

hereby :: thesis: for nt being Symbol of G
for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*>

let t be Symbol of G; :: thesis: ( t in Terminals G implies f . (root-tree t) = <*t*> )
assume t in Terminals G ; :: thesis: f . (root-tree t) = <*t*>
then f . (root-tree t) = s2s . t by A30;
hence f . (root-tree t) = <*t*> by A18; :: thesis: verum

end;

let nt be Symbol of G; :: thesis: for ts being FinSequence of TS G
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*>
let ts be FinSequence of TS G; :: thesis: for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*>
let rts be FinSequence; :: thesis: ( rts = roots ts & nt ==> rts implies for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> )
assume that
A31: rts = roots ts and
A32: nt ==> rts ; :: thesis: for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*>
let x be FinSequence of the carrier of G * ; :: thesis: ( x = f * ts implies f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*> )
assume x = f * ts ; :: thesis: f . (nt -tree ts) = (FlattenSeq x) ^ <*nt*>
hence f . (nt -tree ts) = (FlattenSeq x) ^ (s2s . nt) by A30, A31, A32
.= (FlattenSeq x) ^ <*nt*> by A18 ;
:: thesis: verum