let it1, it2 be FinSequence of the carrier of G; :: thesis: ( ex f being Function of (TS G),( the carrier of 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
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) ) ) & ex f being Function of (TS G),( the carrier of 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
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) ) ) implies it1 = it2 )
given f1 being Function of (TS G),( the carrier of G *) such that A22: it1 = f1 . tsg and
A23: for t being Symbol of G st t in Terminals G holds
f1 . (root-tree t) = <*t*> and
A24: 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 = f1 * ts holds
f1 . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ; :: thesis: ( for f being Function of (TS G),( the carrier of 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 ex rts being FinSequence st
( rts = roots ts & nt ==> rts & ex x being FinSequence of the carrier of G * st
( x = f * ts & not f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) ) or it1 = it2 )
given f2 being Function of (TS G),( the carrier of G *) such that A25: it2 = f2 . tsg and
A26: for t being Symbol of G st t in Terminals G holds
f2 . (root-tree t) = <*t*> and
A27: 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 = f2 * ts holds
f2 . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ; :: thesis: it1 = it2

A28: 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 t in Terminals G ; :: thesis: f1 . (root-tree t) = H₁₀(t)
hence f1 . (root-tree t) = <*t*> by A23
.= H₁₀(t) by A18 ;
:: thesis: verum

end;

let nt be Symbol of G; :: thesis: for ts being FinSequence of TS G st nt ==> roots ts holds
f1 . (nt -tree ts) = H₁₁(nt, roots ts,f1 * ts)
let ts be FinSequence of TS G; :: thesis: ( nt ==> roots ts implies f1 . (nt -tree ts) = H₁₁(nt, roots ts,f1 * ts) )
assume nt ==> roots ts ; :: thesis: f1 . (nt -tree ts) = H₁₁(nt, roots ts,f1 * ts)
hence f1 . (nt -tree ts) = <*nt*> ^ (FlattenSeq (f1 * ts)) by A24
.= H₁₁(nt, roots ts,f1 * ts) by A18 ;
:: thesis: verum

end;

A29: 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 t in Terminals G ; :: thesis: f2 . (root-tree t) = H₁₀(t)
hence f2 . (root-tree t) = <*t*> by A26
.= H₁₀(t) by A18 ;
:: thesis: verum

end;

let nt be Symbol of G; :: thesis: for ts being FinSequence of TS G st nt ==> roots ts holds
f2 . (nt -tree ts) = H₁₁(nt, roots ts,f2 * ts)
let ts be FinSequence of TS G; :: thesis: ( nt ==> roots ts implies f2 . (nt -tree ts) = H₁₁(nt, roots ts,f2 * ts) )
assume nt ==> roots ts ; :: thesis: f2 . (nt -tree ts) = H₁₁(nt, roots ts,f2 * ts)
hence f2 . (nt -tree ts) = <*nt*> ^ (FlattenSeq (f2 * ts)) by A27
.= H₁₁(nt, roots ts,f2 * ts) by A18 ;
:: thesis: verum

end;

f1 = f2 from DTCONSTR:sch 9(A28, A29);
hence it1 = it2 by A22, A25; :: thesis: verum