defpred S1[ set , set , set , set ] means for a being Element of F2()
for ntv being Function of F2(),F3() st ntv = \$4 holds
ntv . a = F7(\$1,\$2,\$3,a);
defpred S2[ set , set ] means for tv being Function of F2(),F3() st tv = \$2 holds
for a being Element of F2() holds tv . a = F6(\$1,a);
reconsider FAB = Funcs (F2(),F3()) as non empty set ;
reconsider f29 = F5() as Function of (TS F1()),FAB ;
A3: now :: thesis: for x being Element of Terminals F1() ex y being Element of FAB st S2[x,y]
let x be Element of Terminals F1(); :: thesis: ex y being Element of FAB st S2[x,y]
deffunc H1( Element of F2()) -> Element of F3() = F6(x,\$1);
consider y being Function of F2(),F3() such that
A4: for a being Element of F2() holds y . a = H1(a) from ( F2() = dom y & rng y c= F3() ) by FUNCT_2:def 1;
then reconsider y = y as Element of FAB by FUNCT_2:def 2;
take y = y; :: thesis: S2[x,y]
thus S2[x,y] by A4; :: thesis: verum
end;
consider TV being Function of (Terminals F1()),FAB such that
A5: for e being Element of Terminals F1() holds S2[e,TV . e] from deffunc H1( Terminal of F1()) -> Element of FAB = TV . \$1;
A6: now :: thesis: for x being Element of NonTerminals F1()
for y, z being Element of FAB ex fab being Element of FAB st S1[x,y,z,fab]
let x be Element of NonTerminals F1(); :: thesis: for y, z being Element of FAB ex fab being Element of FAB st S1[x,y,z,fab]
let y, z be Element of FAB; :: thesis: ex fab being Element of FAB st S1[x,y,z,fab]
deffunc H2( Element of F2()) -> Element of F3() = F7(x,y,z,\$1);
consider fab being Function of F2(),F3() such that
A7: for a being Element of F2() holds fab . a = H2(a) from ( F2() = dom fab & rng fab c= F3() ) by FUNCT_2:def 1;
then reconsider fab = fab as Element of FAB by FUNCT_2:def 2;
take fab = fab; :: thesis: S1[x,y,z,fab]
thus S1[x,y,z,fab] by A7; :: thesis: verum
end;
consider NTV being Function of [:(NonTerminals F1()),FAB,FAB:],FAB such that
A8: for x being Element of NonTerminals F1()
for y, z being Element of FAB holds S1[x,y,z,NTV . [x,y,z]] from deffunc H2( NonTerminal of F1(), set , set , Element of FAB, Element of FAB) -> Element of FAB = NTV . [\$1,\$4,\$5];
A9: now :: thesis: ( ( for t being Terminal of F1() holds f29 . () = H1(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 FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) )
hereby :: 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 FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)
let t be Terminal of F1(); :: thesis: f29 . () = H1(t)
consider TVt being Function such that
A10: TV . t = TVt and
A11: dom TVt = F2() and
A12: rng TVt c= F3() by FUNCT_2:def 2;
reconsider TVt = TVt as Function of F2(),F3() by ;
consider g being Function of F2(),F3() such that
A13: g = F5() . () and
A14: for a being Element of F2() holds g . a = F6(t,a) by A2;
now :: thesis: ( F2() = dom g & F2() = dom TVt & ( for x being object st x in F2() holds
g . x = TVt . x ) )
thus F2() = dom g by FUNCT_2:def 1; :: thesis: ( F2() = dom TVt & ( for x being object st x in F2() holds
g . x = TVt . x ) )

thus F2() = dom TVt by A11; :: thesis: for x being object st x in F2() holds
g . x = TVt . x

let x be object ; :: thesis: ( x in F2() implies g . x = TVt . x )
assume x in F2() ; :: thesis: g . x = TVt . x
then reconsider xx = x as Element of F2() ;
g . xx = F6(t,xx) by A14
.= TVt . xx by ;
hence g . x = TVt . x ; :: thesis: verum
end;
hence f29 . () = H1(t) by ; :: thesis: verum
end;
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 FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(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 FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(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 FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) )

assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)

then consider g, ff1, ff2 being Function of F2(),F3() such that
A15: g = F5() . (nt -tree (tl,tr)) and
A16: ( ff1 = F5() . tl & ff2 = F5() . tr & ( for a being Element of F2() holds g . a = F7(nt,ff1,ff2,a) ) ) by A2;
let xl, xr be Element of FAB; :: thesis: ( xl = f29 . tl & xr = f29 . tr implies f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) )
consider ntvnt being Function such that
A17: ntvnt = NTV . [nt,xl,xr] and
A18: ( dom ntvnt = F2() & rng ntvnt c= F3() ) by FUNCT_2:def 2;
reconsider ntvnt = ntvnt as Function of F2(),F3() by ;
assume A19: ( xl = f29 . tl & xr = f29 . tr ) ; :: thesis: f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)
now :: thesis: ( F2() = dom g & F2() = dom ntvnt & ( for x being object st x in F2() holds
g . x = ntvnt . x ) )
thus F2() = dom g by FUNCT_2:def 1; :: thesis: ( F2() = dom ntvnt & ( for x being object st x in F2() holds
g . x = ntvnt . x ) )

thus F2() = dom ntvnt by FUNCT_2:def 1; :: thesis: for x being object st x in F2() holds
g . x = ntvnt . x

let x be object ; :: thesis: ( x in F2() implies g . x = ntvnt . x )
assume x in F2() ; :: thesis: g . x = ntvnt . x
then reconsider xx = x as Element of F2() ;
g . xx = F7(nt,xl,xr,xx) by
.= ntvnt . xx by ;
hence g . x = ntvnt . x ; :: thesis: verum
end;
hence f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) by ; :: thesis: verum
end;
reconsider f19 = F4() as Function of (TS F1()),FAB ;
A20: now :: thesis: ( ( for t being Terminal of F1() holds f19 . () = H1(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 FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) )
hereby :: 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 FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)
let t be Terminal of F1(); :: thesis: f19 . () = H1(t)
consider TVt being Function such that
A21: TV . t = TVt and
A22: dom TVt = F2() and
A23: rng TVt c= F3() by FUNCT_2:def 2;
reconsider TVt = TVt as Function of F2(),F3() by ;
consider g being Function of F2(),F3() such that
A24: g = F4() . () and
A25: for a being Element of F2() holds g . a = F6(t,a) by A1;
now :: thesis: ( F2() = dom g & F2() = dom TVt & ( for x being object st x in F2() holds
g . x = TVt . x ) )
thus F2() = dom g by FUNCT_2:def 1; :: thesis: ( F2() = dom TVt & ( for x being object st x in F2() holds
g . x = TVt . x ) )

thus F2() = dom TVt by A22; :: thesis: for x being object st x in F2() holds
g . x = TVt . x

let x be object ; :: thesis: ( x in F2() implies g . x = TVt . x )
assume x in F2() ; :: thesis: g . x = TVt . x
then reconsider xx = x as Element of F2() ;
g . xx = F6(t,xx) by A25
.= TVt . xx by ;
hence g . x = TVt . x ; :: thesis: verum
end;
hence f19 . () = H1(t) by ; :: thesis: verum
end;
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 FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(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 FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(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 FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) )

assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)

then consider g, ff1, ff2 being Function of F2(),F3() such that
A26: g = F4() . (nt -tree (tl,tr)) and
A27: ( ff1 = F4() . tl & ff2 = F4() . tr & ( for a being Element of F2() holds g . a = F7(nt,ff1,ff2,a) ) ) by A1;
let xl, xr be Element of FAB; :: thesis: ( xl = f19 . tl & xr = f19 . tr implies f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) )
consider ntvnt being Function such that
A28: ntvnt = NTV . [nt,xl,xr] and
A29: ( dom ntvnt = F2() & rng ntvnt c= F3() ) by FUNCT_2:def 2;
reconsider ntvnt = ntvnt as Function of F2(),F3() by ;
assume A30: ( xl = f19 . tl & xr = f19 . tr ) ; :: thesis: f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)
now :: thesis: ( F2() = dom g & F2() = dom ntvnt & ( for x being object st x in F2() holds
g . x = ntvnt . x ) )
thus F2() = dom g by FUNCT_2:def 1; :: thesis: ( F2() = dom ntvnt & ( for x being object st x in F2() holds
g . x = ntvnt . x ) )

thus F2() = dom ntvnt by FUNCT_2:def 1; :: thesis: for x being object st x in F2() holds
g . x = ntvnt . x

let x be object ; :: thesis: ( x in F2() implies g . x = ntvnt . x )
assume x in F2() ; :: thesis: g . x = ntvnt . x
then reconsider xx = x as Element of F2() ;
g . xx = F7(nt,xl,xr,xx) by
.= ntvnt . xx by ;
hence g . x = ntvnt . x ; :: thesis: verum
end;
hence f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) by ; :: thesis: verum
end;
f19 = f29 from hence F4() = F5() ; :: thesis: verum