deffunc H₁( Symbol of F₁(), FinSequence, FinSequence of F₂()) -> Element of F₂() = F₄($1,($2 . 1),($2 . 2),($3 . 1),($3 . 2));
consider f being Function of (TS F₁()),F₂() such that
A1: for t being Symbol of F₁() st t in Terminals F₁() holds
f . (root-tree t) = F₃(t) and
A2: for nt being Symbol of F₁()
for ts being FinSequence of TS F₁() st nt ==> roots ts holds
f . (nt -tree ts) = H₁(nt, roots ts,f * ts) from DTCONSTR:sch 8();
take f ; :: thesis: ( ( for t being Terminal of F₁() holds f . (root-tree t) = F₃(t) ) & ( for nt being NonTerminal of F₁()
for tl, tr being Element of TS F₁()
for rtl, rtr being Symbol of F₁() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F₂() st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = F₄(nt,rtl,rtr,xl,xr) ) )
A3: dom f = TS F₁() by FUNCT_2:def 1;
thus for t being Terminal of F₁() holds f . (root-tree t) = F₃(t) by A1; :: thesis: for nt being NonTerminal of F₁()
for tl, tr being Element of TS F₁()
for rtl, rtr being Symbol of F₁() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F₂() st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = F₄(nt,rtl,rtr,xl,xr)
let nt be NonTerminal of F₁(); :: thesis: for tl, tr being Element of TS F₁()
for rtl, rtr being Symbol of F₁() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F₂() st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = F₄(nt,rtl,rtr,xl,xr)
let tl, tr be Element of TS F₁(); :: thesis: for rtl, rtr being Symbol of F₁() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F₂() st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = F₄(nt,rtl,rtr,xl,xr)
let rtl, rtr be Symbol of F₁(); :: thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of F₂() st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = F₄(nt,rtl,rtr,xl,xr) )
assume A4: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of F₂() st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = F₄(nt,rtl,rtr,xl,xr)
let xl, xr be Element of F₂(); :: thesis: ( xl = f . tl & xr = f . tr implies f . (nt -tree tl,tr) = F₄(nt,rtl,rtr,xl,xr) )
assume A5: ( xl = f . tl & xr = f . tr ) ; :: thesis: f . (nt -tree tl,tr) = F₄(nt,rtl,rtr,xl,xr)
reconsider ts = <*tl,tr*> as FinSequence of TS F₁() ;
reconsider rts = <*rtl,rtr*> as FinSequence ;
A6: ( ts . 1 = tl & ts . 2 = tr & rts . 1 = rtl & rts . 2 = rtr ) by FINSEQ_1:61;
A7: dom rts = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
A8: dom ts = {1,2} by FINSEQ_1:4, FINSEQ_3:29;

now

let i be Element of NAT ; :: thesis: ( i in dom ts implies ex T being DecoratedTree st
( b₂ = ts . T & rts . T = b₂ . {} ) )
assume i in dom ts ; :: thesis: ex T being DecoratedTree st
( b₂ = ts . T & rts . T = b₂ . {} )
then i in Seg (len ts) by FINSEQ_1:def 3;
then A9: i in Seg 2 by FINSEQ_1:61;

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

suppose i = 1 ; :: thesis: ex T being DecoratedTree st
( b₂ = ts . T & rts . T = b₂ . {} )

hence ex T being DecoratedTree st
( T = ts . i & rts . i = T . {} ) by A4, A6; :: thesis: verum

end;

suppose i = 2 ; :: thesis: ex T being DecoratedTree st
( b₂ = ts . T & rts . T = b₂ . {} )

hence ex T being DecoratedTree st
( T = ts . i & rts . i = T . {} ) by A4, A6; :: thesis: verum

end;

end;

end;

then A10: rts = roots ts by A7, A8, TREES_3:def 18;
reconsider x = <*xl,xr*> as FinSequence of F₂() ;
A11: dom x = {1,2} by FINSEQ_1:4, FINSEQ_3:29;

A12: now

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

A13: now

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

per cases ( y = 1 or y = 2 ) by A11, A14, TARSKI:def 2;

suppose y = 1 ; :: thesis: ( y in dom ts & ts . y in dom f )

hence ( y in dom ts & ts . y in dom f ) by A3, A6, A8, TARSKI:def 2; :: thesis: verum

end;

suppose y = 2 ; :: thesis: ( y in dom ts & ts . y in dom f )

hence ( y in dom ts & ts . y in dom f ) by A3, A6, A8, TARSKI:def 2; :: thesis: verum

end;

end;

end;

now

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

per cases ( y = 1 or y = 2 ) by A8, A15, TARSKI:def 2;

suppose y = 1 ; :: thesis: y in dom x

hence y in dom x by A11, TARSKI:def 2; :: thesis: verum

end;

suppose y = 2 ; :: thesis: y in dom x

hence y in dom x by A11, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence ( y in dom x iff ( y in dom ts & ts . y in dom f ) ) by A13; :: thesis: verum

end;

now

let y be set ; :: 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 A11, TARSKI:def 2;
hence x . y = f . (ts . y) by A5, A6, FINSEQ_1:61; :: thesis: verum

end;

then x = f * ts by A12, FUNCT_1:20;
then A16: f . (nt -tree ts) = F₄(nt,(rts . 1),(rts . 2),(x . 1),(x . 2)) by A2, A4, A10;
( rts . 1 = rtl & rts . 2 = rtr & x . 1 = xl & x . 2 = xr ) by FINSEQ_1:61;
hence f . (nt -tree tl,tr) = F₄(nt,rtl,rtr,xl,xr) by A16, TREES_4:def 6; :: thesis: verum