defpred S₁[ set , set , set , set ] means for a being Element of F₂()
for ntv being Function of F₂(),F₃() st ntv = $4 holds
ntv . a = F₇($1,$2,$3,a);
defpred S₂[ set , set ] means for tv being Function of F₂(),F₃() st tv = $2 holds
for a being Element of F₂() holds tv . a = F₆($1,a);
reconsider FAB = Funcs (F₂(),F₃()) as non empty set ;
reconsider f29 = F₅() as Function of (TS F₁()),FAB ;

let x be Element of Terminals F₁(); :: thesis:
deffunc H₁( Element of F₂()) -> Element of F₃() = F₆(x,$1);
consider y being Function of F₂(),F₃() such that
A4: for a being Element of F₂() holds y . a = H₁(a) from FUNCT_2:sch 4();
( F₂() = dom y & rng y c= F₃() ) by FUNCT_2:def 1;
then reconsider y = y as Element of FAB by FUNCT_2:def 2;
take y = y; :: thesis:
thus S₂[x,y] by A4; :: thesis:

end;

consider TV being Function of (Terminals F₁()),FAB such that
A5: for e being Element of Terminals F₁() holds S₂[e,TV . e] from FUNCT_2:sch 3(A3);
deffunc H₁( Terminal of F₁()) -> Element of FAB = TV . $1;

A6: now :: thesis:

let x be Element of NonTerminals F₁(); :: thesis:
let y, z be Element of FAB; :: thesis:
deffunc H₂( Element of F₂()) -> Element of F₃() = F₇(x,y,z,$1);
consider fab being Function of F₂(),F₃() such that
A7: for a being Element of F₂() holds fab . a = H₂(a) from FUNCT_2:sch 4();
( F₂() = dom fab & rng fab c= F₃() ) by FUNCT_2:def 1;
then reconsider fab = fab as Element of FAB by FUNCT_2:def 2;
take fab = fab; :: thesis:
thus S₁[x,y,z,fab] by A7; :: thesis:

end;

consider NTV being Function of [:(NonTerminals F₁()),FAB,FAB:],FAB such that
A8: for x being Element of NonTerminals F₁()
for y, z being Element of FAB holds S₁[x,y,z,NTV . [x,y,z]] from MULTOP_1:sch 1(A6);
deffunc H₂( NonTerminal of F₁(), set , set , Element of FAB, Element of FAB) -> Element of FAB = NTV . [$1,$4,$5];

A9: now :: thesis:

hereby :: thesis:

let t be Terminal of F₁(); :: thesis:
consider TVt being Function such that
A10: TV . t = TVt and
A11: dom TVt = F₂() and
A12: rng TVt c= F₃() by FUNCT_2:def 2;
reconsider TVt = TVt as Function of F₂(),F₃() by A11, A12, FUNCT_2:def 1, RELSET_1:4;
consider g being Function of F₂(),F₃() such that
A13: g = F₅() . (root-tree t) and
A14: for a being Element of F₂() holds g . a = F₆(t,a) by A2;

now :: thesis:

thus F₂() = dom g by FUNCT_2:def 1; :: thesis:
thus F₂() = dom TVt by A11; :: thesis:
let x be object ; :: thesis:
assume x in F₂() ; :: thesis:
then reconsider xx = x as Element of F₂() ;
g . xx = F₆(t,xx) by A14
.= TVt . xx by A5, A10 ;
hence g . x = TVt . x ; :: thesis:

end;

hence f29 . (root-tree t) = H₁(t) by A13, A10, FUNCT_1:2; :: thesis:

end;

let nt be NonTerminal of F₁(); :: thesis:
let tl, tr be Element of TS F₁(); :: thesis:
let rtl, rtr be Symbol of F₁(); :: thesis:
assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis:
then consider g, ff1, ff2 being Function of F₂(),F₃() such that
A15: g = F₅() . (nt -tree (tl,tr)) and
A16: ( ff1 = F₅() . tl & ff2 = F₅() . tr & ( for a being Element of F₂() holds g . a = F₇(nt,ff1,ff2,a) ) ) by A2;
let xl, xr be Element of FAB; :: thesis:
consider ntvnt being Function such that
A17: ntvnt = NTV . [nt,xl,xr] and
A18: ( dom ntvnt = F₂() & rng ntvnt c= F₃() ) by FUNCT_2:def 2;
reconsider ntvnt = ntvnt as Function of F₂(),F₃() by A18, FUNCT_2:def 1, RELSET_1:4;
assume A19: ( xl = f29 . tl & xr = f29 . tr ) ; :: thesis:

now :: thesis:

thus F₂() = dom g by FUNCT_2:def 1; :: thesis:
thus F₂() = dom ntvnt by FUNCT_2:def 1; :: thesis:
let x be object ; :: thesis:
assume x in F₂() ; :: thesis:
then reconsider xx = x as Element of F₂() ;
g . xx = F₇(nt,xl,xr,xx) by A19, A16
.= ntvnt . xx by A8, A17 ;
hence g . x = ntvnt . x ; :: thesis:

end;

hence f29 . (nt -tree (tl,tr)) = H₂(nt,rtl,rtr,xl,xr) by A15, A17, FUNCT_1:2; :: thesis:

end;

reconsider f19 = F₄() as Function of (TS F₁()),FAB ;

A20: now :: thesis:

hereby :: thesis:

let t be Terminal of F₁(); :: thesis:
consider TVt being Function such that
A21: TV . t = TVt and
A22: dom TVt = F₂() and
A23: rng TVt c= F₃() by FUNCT_2:def 2;
reconsider TVt = TVt as Function of F₂(),F₃() by A22, A23, FUNCT_2:def 1, RELSET_1:4;
consider g being Function of F₂(),F₃() such that
A24: g = F₄() . (root-tree t) and
A25: for a being Element of F₂() holds g . a = F₆(t,a) by A1;

now :: thesis:

thus F₂() = dom g by FUNCT_2:def 1; :: thesis:
thus F₂() = dom TVt by A22; :: thesis:
let x be object ; :: thesis:
assume x in F₂() ; :: thesis:
then reconsider xx = x as Element of F₂() ;
g . xx = F₆(t,xx) by A25
.= TVt . xx by A5, A21 ;
hence g . x = TVt . x ; :: thesis:

end;

hence f19 . (root-tree t) = H₁(t) by A24, A21, FUNCT_1:2; :: thesis:

end;

let nt be NonTerminal of F₁(); :: thesis:
let tl, tr be Element of TS F₁(); :: thesis:
let rtl, rtr be Symbol of F₁(); :: thesis:
assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis:
then consider g, ff1, ff2 being Function of F₂(),F₃() such that
A26: g = F₄() . (nt -tree (tl,tr)) and
A27: ( ff1 = F₄() . tl & ff2 = F₄() . tr & ( for a being Element of F₂() holds g . a = F₇(nt,ff1,ff2,a) ) ) by A1;
let xl, xr be Element of FAB; :: thesis:
consider ntvnt being Function such that
A28: ntvnt = NTV . [nt,xl,xr] and
A29: ( dom ntvnt = F₂() & rng ntvnt c= F₃() ) by FUNCT_2:def 2;
reconsider ntvnt = ntvnt as Function of F₂(),F₃() by A29, FUNCT_2:def 1, RELSET_1:4;
assume A30: ( xl = f19 . tl & xr = f19 . tr ) ; :: thesis:

now :: thesis:

thus F₂() = dom g by FUNCT_2:def 1; :: thesis:
thus F₂() = dom ntvnt by FUNCT_2:def 1; :: thesis:
let x be object ; :: thesis:
assume x in F₂() ; :: thesis:
then reconsider xx = x as Element of F₂() ;
g . xx = F₇(nt,xl,xr,xx) by A30, A27
.= ntvnt . xx by A8, A28 ;
hence g . x = ntvnt . x ; :: thesis:

end;

hence f19 . (nt -tree (tl,tr)) = H₂(nt,rtl,rtr,xl,xr) by A26, A28, FUNCT_1:2; :: thesis:

end;

f19 = f29 from BINTREE1:sch 4(A20, A9);
hence F₄() = F₅() ; :: thesis: