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) ) )
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 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₂() st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = F₄(nt,rtl,rtr,xl,xr)
reconsider rts = <*rtl,rtr*> as FinSequence ;
reconsider ts = <*tl,tr*> as FinSequence of TS F₁() ;
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) )
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;
A10: dom f = TS F₁() by FUNCT_2:def 1;

A11: now :: thesis: for y being object holds
( 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 ) )

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

per cases ( y = 1 or y = 2 ) by A7, A13, TARSKI:def 2;

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

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

end;

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

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

end;

end;

end;

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

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

per cases ( y = 1 or y = 2 ) by A8, 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 A10, A7, 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 A10, A7, TARSKI:def 2; :: thesis: verum

end;

end;

end;

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

end;

assume A15: ( xl = f . tl & xr = f . tr ) ; :: thesis: f . (nt -tree (tl,tr)) = F₄(nt,rtl,rtr,xl,xr)

now :: thesis: for y being object st y in dom x holds
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; :: thesis: verum

end;

then A16: x = f * ts by A11, FUNCT_1:10;

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 . {} )

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 A20: i in Seg 2 by FINSEQ_1:44;

per cases ( i = 1 or i = 2 ) by A20, FINSEQ_1:2, 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 A3; :: 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; :: thesis: verum

end;

end;

end;

dom rts = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then rts = roots ts by A7, A19, TREES_3:def 18;
then A21: f . (nt -tree ts) = F₄(nt,(rts . 1),(rts . 2),(x . 1),(x . 2)) by A2, A5, A16;
thus f . (nt -tree (tl,tr)) = F₄(nt,rtl,rtr,xl,xr) by A21, TREES_4:def 6; :: thesis: verum