deffunc H1( Symbol of F1(), FinSequence, FinSequence of F2()) -> Element of F2() = F4(\$1,(\$2 . 1),(\$2 . 2),(\$3 . 1),(\$3 . 2));
consider f being Function of (TS F1()),F2() such that
A1: for t being Symbol of F1() st t in Terminals F1() holds
f . () = F3(t) and
A2: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
f . (nt -tree ts) = H1(nt, roots ts,f * ts) from take f ; :: thesis: ( ( for t being Terminal of F1() holds f . () = F3(t) ) & ( for nt being NonTerminal of F1()
for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) ) )

thus for t being Terminal of F1() holds f . () = F3(t) by A1; :: thesis: for nt being NonTerminal of F1()
for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr)

let nt be NonTerminal of F1(); :: thesis: for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr)

let tl, tr be Element of TS F1(); :: thesis: for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr)

let rtl, rtr be Symbol of F1(); :: thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = F4(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 F2() st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr)

reconsider rts = <*rtl,rtr*> as FinSequence ;
reconsider ts = <*tl,tr*> as FinSequence of TS F1() ;
A6: ts . 1 = tl by FINSEQ_1:44;
let xl, xr be Element of F2(); :: thesis: ( xl = f . tl & xr = f . tr implies f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) )
A7: dom ts = {1,2} by ;
reconsider x = <*xl,xr*> as FinSequence of F2() ;
A8: dom x = {1,2} by ;
A9: ts . 2 = tr by FINSEQ_1:44;
A10: dom f = TS F1() 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 ;
suppose y = 1 ; :: thesis: y in dom x
hence y in dom x by ; :: thesis: verum
end;
suppose y = 2 ; :: thesis: y in dom x
hence y in dom x by ; :: 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 ;
suppose y = 1 ; :: thesis: ( y in dom ts & ts . y in dom f )
hence ( y in dom ts & ts . y in dom f ) by ; :: 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 ; :: 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)) = F4(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 ;
hence x . y = f . (ts . y) by ; :: thesis: verum
end;
then A16: x = f * ts by ;
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 . {} )
let i be Element of NAT ; :: thesis: ( i in dom ts implies ex T being DecoratedTree st
( b2 = ts . T & rts . T = b2 . {} ) )

assume i in dom ts ; :: thesis: ex T being DecoratedTree st
( b2 = ts . T & rts . T = b2 . {} )

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 ;
suppose i = 1 ; :: thesis: ex T being DecoratedTree st
( b2 = ts . T & rts . T = b2 . {} )

hence ex T being DecoratedTree st
( T = ts . i & rts . i = T . {} ) by A3, A6, A18; :: thesis: verum
end;
suppose i = 2 ; :: thesis: ex T being DecoratedTree st
( b2 = ts . T & rts . T = b2 . {} )

hence ex T being DecoratedTree st
( T = ts . i & rts . i = T . {} ) by A4, A9, A17; :: thesis: verum
end;
end;
end;
dom rts = {1,2} by ;
then rts = roots ts by ;
then A21: f . (nt -tree ts) = F4(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)) = F4(nt,rtl,rtr,xl,xr) by ; :: thesis: verum