reconsider FAB = Funcs F₂(),F₃() as non empty set ;
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);

A3: now

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);
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);

A6: now

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);
reconsider f1' = F₄() as Function of TS F₁(),FAB ;
reconsider f2' = F₅() as Function of TS F₁(),FAB ;
deffunc H₁( Terminal of F₁()) -> Element of FAB = TV . $1;
deffunc H₂( NonTerminal of F₁(), set , set , Element of FAB, Element of FAB) -> Element of FAB = NTV . [$1,$4,$5];

A9: now

hereby :: thesis:

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

now

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

end;

hence f1' . (root-tree t) = H₁(t) by A10, A11, FUNCT_1:9; :: 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 A12: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis:
let xl, xr be Element of FAB; :: thesis:
assume A13: ( xl = f1' . tl & xr = f1' . tr ) ; :: thesis:
consider g, ff1, ff2 being Function of F₂(),F₃() such that
A14: ( g = F₄() . (nt -tree tl,tr) & ff1 = F₄() . tl & ff2 = F₄() . tr & ( for a being Element of F₂() holds g . a = F₇(nt,ff1,ff2,a) ) ) by A1, A12;
consider ntvnt being Function such that
A15: ( ntvnt = NTV . [nt,xl,xr] & dom ntvnt = F₂() & rng ntvnt c= F₃() ) by FUNCT_2:def 2;
reconsider ntvnt = ntvnt as Function of F₂(),F₃() by A15, FUNCT_2:def 1, RELSET_1:11;

now

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

end;

hence f1' . (nt -tree tl,tr) = H₂(nt,rtl,rtr,xl,xr) by A14, A15, FUNCT_1:9; :: thesis:

end;

A16: now

hereby :: thesis:

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

now

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

end;

hence f2' . (root-tree t) = H₁(t) by A17, A18, FUNCT_1:9; :: 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 A19: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis:
let xl, xr be Element of FAB; :: thesis:
assume A20: ( xl = f2' . tl & xr = f2' . tr ) ; :: thesis:
consider g, ff1, ff2 being Function of F₂(),F₃() such that
A21: ( g = F₅() . (nt -tree tl,tr) & ff1 = F₅() . tl & ff2 = F₅() . tr & ( for a being Element of F₂() holds g . a = F₇(nt,ff1,ff2,a) ) ) by A2, A19;
consider ntvnt being Function such that
A22: ( ntvnt = NTV . [nt,xl,xr] & dom ntvnt = F₂() & rng ntvnt c= F₃() ) by FUNCT_2:def 2;
reconsider ntvnt = ntvnt as Function of F₂(),F₃() by A22, FUNCT_2:def 1, RELSET_1:11;

now

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

end;

hence f2' . (nt -tree tl,tr) = H₂(nt,rtl,rtr,xl,xr) by A21, A22, FUNCT_1:9; :: thesis:

end;

f1' = f2' from BINTREE1:sch 4(A9, A16);
hence F₄() = F₅() ; :: thesis: