deffunc H1( Symbol of F1(), FinSequence, FinSequence of F2()) -> Element of F2() = F6(\$1,(\$2 . 1),(\$2 . 2),(\$3 . 1),(\$3 . 2));
A3: now :: thesis: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F4() . () = F5(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) ) )
thus for t being Symbol of F1() st t in Terminals F1() holds
F4() . () = F5(t) by A2; :: thesis: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts)

let nt be Symbol of F1(); :: thesis: for ts being FinSequence of TS F1() st nt ==> roots ts holds
F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts)

let ts be FinSequence of TS F1(); :: thesis: ( nt ==> roots ts implies F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) )
set rts = roots ts;
set x = F4() * ts;
assume A4: nt ==> roots ts ; :: thesis: F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts)
then consider tl, tr being Element of TS F1() such that
A5: roots ts = <*(),()*> and
A6: tl = ts . 1 and
A7: tr = ts . 2 and
A8: nt -tree ts = nt -tree (tl,tr) and
tl in rng ts and
tr in rng ts by Th10;
A9: nt is NonTerminal of F1() by ;
reconsider xr = F4() . tr as Element of F2() ;
2 in dom ts by ;
then A10: (F4() * ts) . 2 = xr by ;
reconsider xl = F4() . tl as Element of F2() ;
1 in dom ts by ;
then A11: (F4() * ts) . 1 = xl by ;
( root-label tl = (roots ts) . 1 & root-label tr = (roots ts) . 2 ) by ;
hence F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) by A2, A4, A5, A8, A9, A11, A10; :: thesis: verum
end;
A12: now :: thesis: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F3() . () = F5(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) ) )
thus for t being Symbol of F1() st t in Terminals F1() holds
F3() . () = F5(t) by A1; :: thesis: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts)

let nt be Symbol of F1(); :: thesis: for ts being FinSequence of TS F1() st nt ==> roots ts holds
F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts)

let ts be FinSequence of TS F1(); :: thesis: ( nt ==> roots ts implies F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) )
set rts = roots ts;
set x = F3() * ts;
assume A13: nt ==> roots ts ; :: thesis: F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts)
then consider tl, tr being Element of TS F1() such that
A14: roots ts = <*(),()*> and
A15: tl = ts . 1 and
A16: tr = ts . 2 and
A17: nt -tree ts = nt -tree (tl,tr) and
tl in rng ts and
tr in rng ts by Th10;
A18: nt is NonTerminal of F1() by ;
reconsider xr = F3() . tr as Element of F2() ;
2 in dom ts by ;
then A19: (F3() * ts) . 2 = xr by ;
reconsider xl = F3() . tl as Element of F2() ;
1 in dom ts by ;
then A20: (F3() * ts) . 1 = xl by ;
( root-label tl = (roots ts) . 1 & root-label tr = (roots ts) . 2 ) by ;
hence F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) by A1, A13, A14, A17, A18, A20, A19; :: thesis: verum
end;
thus F3() = F4() from :: thesis: verum