deffunc H₁₂( Symbol of G) -> Element of the carrier of G * = s2s . $1;
deffunc H₁₃( Symbol of G, set , FinSequence of the carrier of G * ) -> Element of the carrier of G * = (s2s . $1) ^ (FlattenSeq $3);
consider f being Function of (TS G),( the carrier of G *) such that
A19: ( ( 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) = <*nt*> ^ (FlattenSeq x) ) )
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) = <*nt*> ^ (FlattenSeq x) ) )
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) = <*nt*> ^ (FlattenSeq x) ) )

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) = <*nt*> ^ (FlattenSeq x)

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 A19;
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) = <*nt*> ^ (FlattenSeq x)
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) = <*nt*> ^ (FlattenSeq x)
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) = <*nt*> ^ (FlattenSeq x) )
assume that
A20: rts = roots ts and
A21: nt ==> rts ; :: thesis: for x being FinSequence of the carrier of G * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x)
let x be FinSequence of the carrier of G * ; :: thesis: ( x = f * ts implies f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) )
assume x = f * ts ; :: thesis: f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x)
hence f . (nt -tree ts) = (s2s . nt) ^ (FlattenSeq x) by A19, A20, A21
.= <*nt*> ^ (FlattenSeq x) by A18 ;
:: thesis: verum