deffunc H_{1}( Symbol of F_{1}(), FinSequence, FinSequence of F_{2}()) -> Element of F_{2}() = F_{4}($1,($2 . 1),($2 . 2),($3 . 1),($3 . 2));

consider f being Function of (TS F_{1}()),F_{2}() such that

A1: for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

f . (root-tree t) = F_{3}(t)
and

A2: for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

f . (nt -tree ts) = H_{1}(nt, roots ts,f * ts)
from DTCONSTR:sch 8();

take f ; :: thesis: ( ( for t being Terminal of F_{1}() holds f . (root-tree t) = F_{3}(t) ) & ( for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of F_{2}() st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = F_{4}(nt,rtl,rtr,xl,xr) ) )

thus for t being Terminal of F_{1}() holds f . (root-tree t) = F_{3}(t)
by A1; :: thesis: for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of F_{2}() st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = F_{4}(nt,rtl,rtr,xl,xr)

let nt be NonTerminal of F_{1}(); :: thesis: for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of F_{2}() st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = F_{4}(nt,rtl,rtr,xl,xr)

let tl, tr be Element of TS F_{1}(); :: thesis: for rtl, rtr being Symbol of F_{1}() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of F_{2}() st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = F_{4}(nt,rtl,rtr,xl,xr)

let rtl, rtr be Symbol of F_{1}(); :: thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of F_{2}() st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = F_{4}(nt,rtl,rtr,xl,xr) )

assume that

A3: rtl = root-label tl and

A4: rtr = root-label tr and

A5: nt ==> <*rtl,rtr*> ; :: thesis: for xl, xr being Element of F_{2}() st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = F_{4}(nt,rtl,rtr,xl,xr)

reconsider rts = <*rtl,rtr*> as FinSequence ;

reconsider ts = <*tl,tr*> as FinSequence of TS F_{1}() ;

A6: ts . 1 = tl by FINSEQ_1:44;

let xl, xr be Element of F_{2}(); :: thesis: ( xl = f . tl & xr = f . tr implies f . (nt -tree (tl,tr)) = F_{4}(nt,rtl,rtr,xl,xr) )

A7: dom ts = {1,2} by FINSEQ_1:2, FINSEQ_1:89;

reconsider x = <*xl,xr*> as FinSequence of F_{2}() ;

A8: dom x = {1,2} by FINSEQ_1:2, FINSEQ_1:89;

A9: ts . 2 = tr by FINSEQ_1:44;

A10: dom f = TS F_{1}()
by FUNCT_2:def 1;

_{4}(nt,rtl,rtr,xl,xr)

A17: rts . 2 = rtr by FINSEQ_1:44;

A18: rts . 1 = rtl by FINSEQ_1:44;

then rts = roots ts by A7, A19, TREES_3:def 18;

then A21: f . (nt -tree ts) = F_{4}(nt,(rts . 1),(rts . 2),(x . 1),(x . 2))
by A2, A5, A16;

A22: ( x . 1 = xl & x . 2 = xr ) by FINSEQ_1:44;

( rts . 1 = rtl & rts . 2 = rtr ) by FINSEQ_1:44;

hence f . (nt -tree (tl,tr)) = F_{4}(nt,rtl,rtr,xl,xr)
by A21, A22, TREES_4:def 6; :: thesis: verum

consider f being Function of (TS F

A1: for t being Symbol of F

f . (root-tree t) = F

A2: for nt being Symbol of F

for ts being FinSequence of TS F

f . (nt -tree ts) = H

take f ; :: thesis: ( ( for t being Terminal of F

for tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of F

f . (nt -tree (tl,tr)) = F

thus for t being Terminal of F

for tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of F

f . (nt -tree (tl,tr)) = F

let nt be NonTerminal of F

for rtl, rtr being Symbol of F

for xl, xr being Element of F

f . (nt -tree (tl,tr)) = F

let tl, tr be Element of TS F

for xl, xr being Element of F

f . (nt -tree (tl,tr)) = F

let rtl, rtr be Symbol of F

f . (nt -tree (tl,tr)) = F

assume that

A3: rtl = root-label tl and

A4: rtr = root-label tr and

A5: nt ==> <*rtl,rtr*> ; :: thesis: for xl, xr being Element of F

f . (nt -tree (tl,tr)) = F

reconsider rts = <*rtl,rtr*> as FinSequence ;

reconsider ts = <*tl,tr*> as FinSequence of TS F

A6: ts . 1 = tl by FINSEQ_1:44;

let xl, xr be Element of F

A7: dom ts = {1,2} by FINSEQ_1:2, FINSEQ_1:89;

reconsider x = <*xl,xr*> as FinSequence of F

A8: dom x = {1,2} by FINSEQ_1:2, FINSEQ_1:89;

A9: ts . 2 = tr by FINSEQ_1:44;

A10: dom f = TS F

A11: now :: thesis: for y being object holds

( y in dom x iff ( y in dom ts & ts . y in dom f ) )

assume A15:
( xl = f . tl & xr = f . tr )
; :: thesis: f . (nt -tree (tl,tr)) = F( y in dom x iff ( y in dom ts & ts . y in dom f ) )

let y be object ; :: thesis: ( y in dom x iff ( y in dom ts & ts . y in dom f ) )

end;A12: now :: thesis: ( y in dom ts & ts . y in dom f implies y in dom x )

assume that

A13: y in dom ts and

ts . y in dom f ; :: thesis: y in dom x

end;A13: y in dom ts and

ts . y in dom f ; :: thesis: y in dom x

now :: thesis: ( y in dom x implies ( y in dom ts & ts . y in dom f ) )

hence
( y in dom x iff ( y in dom ts & ts . y in dom f ) )
by A12; :: thesis: verumassume A14:
y in dom x
; :: thesis: ( y in dom ts & ts . y in dom f )

end;now :: thesis: for y being object st y in dom x holds

x . y = f . (ts . y)

then A16:
x = f * ts
by A11, FUNCT_1:10;x . y = f . (ts . y)

let y be object ; :: thesis: ( y in dom x implies x . y = f . (ts . y) )

assume y in dom x ; :: thesis: x . y = f . (ts . y)

then ( y = 1 or y = 2 ) by A8, TARSKI:def 2;

hence x . y = f . (ts . y) by A15, A6, A9, FINSEQ_1:44; :: thesis: verum

end;assume y in dom x ; :: thesis: x . y = f . (ts . y)

then ( y = 1 or y = 2 ) by A8, TARSKI:def 2;

hence x . y = f . (ts . y) by A15, A6, A9, FINSEQ_1:44; :: thesis: verum

A17: rts . 2 = rtr by FINSEQ_1:44;

A18: rts . 1 = rtl by FINSEQ_1:44;

A19: now :: thesis: for i being Element of NAT st i in dom ts holds

ex T being DecoratedTree st

( T = ts . i & rts . i = T . {} )

dom rts = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;ex T being DecoratedTree st

( T = ts . i & rts . i = T . {} )

let i be Element of NAT ; :: thesis: ( i in dom ts implies ex T being DecoratedTree st

( b_{2} = ts . T & rts . T = b_{2} . {} ) )

assume i in dom ts ; :: thesis: ex T being DecoratedTree st

( b_{2} = ts . T & rts . T = b_{2} . {} )

then i in Seg (len ts) by FINSEQ_1:def 3;

then A20: i in Seg 2 by FINSEQ_1:44;

end;( b

assume i in dom ts ; :: thesis: ex T being DecoratedTree st

( b

then i in Seg (len ts) by FINSEQ_1:def 3;

then A20: i in Seg 2 by FINSEQ_1:44;

per cases
( i = 1 or i = 2 )
by A20, FINSEQ_1:2, TARSKI:def 2;

end;

suppose
i = 1
; :: thesis: ex T being DecoratedTree st

( b_{2} = ts . T & rts . T = b_{2} . {} )

( b

hence
ex T being DecoratedTree st

( T = ts . i & rts . i = T . {} ) by A3, A6, A18; :: thesis: verum

end;( T = ts . i & rts . i = T . {} ) by A3, A6, A18; :: thesis: verum

suppose
i = 2
; :: thesis: ex T being DecoratedTree st

( b_{2} = ts . T & rts . T = b_{2} . {} )

( b

hence
ex T being DecoratedTree st

( T = ts . i & rts . i = T . {} ) by A4, A9, A17; :: thesis: verum

end;( T = ts . i & rts . i = T . {} ) by A4, A9, A17; :: thesis: verum

then rts = roots ts by A7, A19, TREES_3:def 18;

then A21: f . (nt -tree ts) = F

A22: ( x . 1 = xl & x . 2 = xr ) by FINSEQ_1:44;

( rts . 1 = rtl & rts . 2 = rtr ) by FINSEQ_1:44;

hence f . (nt -tree (tl,tr)) = F