defpred S_{1}[ set , set , set , set ] means for a being Element of F_{2}()

for ntv being Function of F_{2}(),F_{3}() st ntv = $4 holds

ntv . a = F_{5}($1,$2,$3,a);

defpred S_{2}[ set , set ] means for tv being Function of F_{2}(),F_{3}() st tv = $2 holds

for a being Element of F_{2}() holds tv . a = F_{4}($1,a);

reconsider FAB = Funcs (F_{2}(),F_{3}()) as non empty set ;

_{1}()),FAB such that

A3: for e being Element of Terminals F_{1}() holds S_{2}[e,TV . e]
from FUNCT_2:sch 3(A1);

deffunc H_{1}( Terminal of F_{1}()) -> Element of FAB = TV . $1;

_{1}()),FAB,FAB:],FAB such that

A6: for x being Element of NonTerminals F_{1}()

for y, z being Element of FAB holds S_{1}[x,y,z,NTV . [x,y,z]]
from MULTOP_1:sch 1(A4);

deffunc H_{2}( Element of NonTerminals F_{1}(), set , set , Element of FAB, Element of FAB) -> Element of FAB = NTV . [$1,$4,$5];

consider f being Function of (TS F_{1}()),FAB such that

A7: ( ( for t being Terminal of F_{1}() holds f . (root-tree t) = H_{1}(t) ) & ( for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds

for xl, xr being Element of FAB st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = H_{2}(nt,rtl,rtr,xl,xr) ) )
from BINTREE1:sch 3();

reconsider f9 = f as Function of (TS F_{1}()),(Funcs (F_{2}(),F_{3}())) ;

take f9 ; :: thesis: ( ( for t being Terminal of F_{1}() ex g being Function of F_{2}(),F_{3}() st

( g = f9 . (root-tree t) & ( for a being Element of F_{2}() holds g . a = F_{4}(t,a) ) ) ) & ( for nt being NonTerminal of F_{1}()

for t1, t2 being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being Function of F_{2}(),F_{3}() st

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F_{2}() holds g . a = F_{5}(nt,f1,f2,a) ) ) ) )

_{1}(); :: thesis: for t1, t2 being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being Function of F_{2}(),F_{3}() st

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F_{2}() holds g . a = F_{5}(nt,f1,f2,a) ) )

let t1, t2 be Element of TS F_{1}(); :: thesis: for rtl, rtr being Symbol of F_{1}() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being Function of F_{2}(),F_{3}() st

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F_{2}() holds g . a = F_{5}(nt,f1,f2,a) ) )

let rtl, rtr be Symbol of F_{1}(); :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, f1, f2 being Function of F_{2}(),F_{3}() st

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F_{2}() holds g . a = F_{5}(nt,f1,f2,a) ) ) )

assume A10: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: ex g, f1, f2 being Function of F_{2}(),F_{3}() st

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F_{2}() holds g . a = F_{5}(nt,f1,f2,a) ) )

ex f2 being Function st

( f . t2 = f2 & dom f2 = F_{2}() & rng f2 c= F_{3}() )
by FUNCT_2:def 2;

then reconsider f2 = f . t2 as Function of F_{2}(),F_{3}() by FUNCT_2:def 1, RELSET_1:4;

ex f1 being Function st

( f . t1 = f1 & dom f1 = F_{2}() & rng f1 c= F_{3}() )
by FUNCT_2:def 2;

then reconsider f1 = f . t1 as Function of F_{2}(),F_{3}() by FUNCT_2:def 1, RELSET_1:4;

NTV . [nt,(f . t1),(f . t2)] in FAB ;

then consider ntvval being Function such that

A11: ntvval = NTV . [nt,f1,f2] and

A12: ( dom ntvval = F_{2}() & rng ntvval c= F_{3}() )
by FUNCT_2:def 2;

reconsider ntvval = ntvval as Function of F_{2}(),F_{3}() by A12, FUNCT_2:def 1, RELSET_1:4;

take ntvval ; :: thesis: ex f1, f2 being Function of F_{2}(),F_{3}() st

( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F_{2}() holds ntvval . a = F_{5}(nt,f1,f2,a) ) )

take f1 ; :: thesis: ex f2 being Function of F_{2}(),F_{3}() st

( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F_{2}() holds ntvval . a = F_{5}(nt,f1,f2,a) ) )

take f2 ; :: thesis: ( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F_{2}() holds ntvval . a = F_{5}(nt,f1,f2,a) ) )

thus ( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 ) by A7, A10, A11; :: thesis: for a being Element of F_{2}() holds ntvval . a = F_{5}(nt,f1,f2,a)

thus for a being Element of F_{2}() holds ntvval . a = F_{5}(nt,f1,f2,a)
by A6, A11; :: thesis: verum

for ntv being Function of F

ntv . a = F

defpred S

for a being Element of F

reconsider FAB = Funcs (F

A1: now :: thesis: for x being Element of Terminals F_{1}() ex y being Element of FAB st S_{2}[x,y]

consider TV being Function of (Terminals Flet x be Element of Terminals F_{1}(); :: thesis: ex y being Element of FAB st S_{2}[x,y]

deffunc H_{1}( set ) -> Element of F_{3}() = F_{4}(x,$1);

consider y being Function of F_{2}(),F_{3}() such that

A2: for a being Element of F_{2}() holds y . a = H_{1}(a)
from FUNCT_2:sch 4();

( F_{2}() = dom y & rng y c= F_{3}() )
by FUNCT_2:def 1;

then reconsider y = y as Element of FAB by FUNCT_2:def 2;

take y = y; :: thesis: S_{2}[x,y]

thus S_{2}[x,y]
by A2; :: thesis: verum

end;deffunc H

consider y being Function of F

A2: for a being Element of F

( F

then reconsider y = y as Element of FAB by FUNCT_2:def 2;

take y = y; :: thesis: S

thus S

A3: for e being Element of Terminals F

deffunc H

A4: now :: thesis: for x being Element of NonTerminals F_{1}()

for y, z being Element of FAB ex fab being Element of FAB st S_{1}[x,y,z,fab]

consider NTV being Function of [:(NonTerminals Ffor y, z being Element of FAB ex fab being Element of FAB st S

let x be Element of NonTerminals F_{1}(); :: thesis: for y, z being Element of FAB ex fab being Element of FAB st S_{1}[x,y,z,fab]

let y, z be Element of FAB; :: thesis: ex fab being Element of FAB st S_{1}[x,y,z,fab]

deffunc H_{2}( set ) -> Element of F_{3}() = F_{5}(x,y,z,$1);

consider fab being Function of F_{2}(),F_{3}() such that

A5: for a being Element of F_{2}() holds fab . a = H_{2}(a)
from FUNCT_2:sch 4();

( F_{2}() = dom fab & rng fab c= F_{3}() )
by FUNCT_2:def 1;

then reconsider fab = fab as Element of FAB by FUNCT_2:def 2;

take fab = fab; :: thesis: S_{1}[x,y,z,fab]

thus S_{1}[x,y,z,fab]
by A5; :: thesis: verum

end;let y, z be Element of FAB; :: thesis: ex fab being Element of FAB st S

deffunc H

consider fab being Function of F

A5: for a being Element of F

( F

then reconsider fab = fab as Element of FAB by FUNCT_2:def 2;

take fab = fab; :: thesis: S

thus S

A6: for x being Element of NonTerminals F

for y, z being Element of FAB holds S

deffunc H

consider f being Function of (TS F

A7: ( ( for t being Terminal of F

for tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of FAB st xl = f . tl & xr = f . tr holds

f . (nt -tree (tl,tr)) = H

reconsider f9 = f as Function of (TS F

take f9 ; :: thesis: ( ( for t being Terminal of F

( g = f9 . (root-tree t) & ( for a being Element of F

for t1, t2 being Element of TS F

for rtl, rtr being Symbol of F

ex g, f1, f2 being Function of F

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F

hereby :: thesis: for nt being NonTerminal of F_{1}()

for t1, t2 being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, f1, f2 being Function of F_{2}(),F_{3}() st

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F_{2}() holds g . a = F_{5}(nt,f1,f2,a) ) )

let nt be NonTerminal of Ffor t1, t2 being Element of TS F

for rtl, rtr being Symbol of F

ex g, f1, f2 being Function of F

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F

let t be Terminal of F_{1}(); :: thesis: ex TVt being Function of F_{2}(),F_{3}() st

( TVt = f9 . (root-tree t) & ( for a being Element of F_{2}() holds TVt . a = F_{4}(t,a) ) )

consider TVt being Function such that

A8: TV . t = TVt and

A9: ( dom TVt = F_{2}() & rng TVt c= F_{3}() )
by FUNCT_2:def 2;

reconsider TVt = TVt as Function of F_{2}(),F_{3}() by A9, FUNCT_2:def 1, RELSET_1:4;

take TVt = TVt; :: thesis: ( TVt = f9 . (root-tree t) & ( for a being Element of F_{2}() holds TVt . a = F_{4}(t,a) ) )

thus TVt = f9 . (root-tree t) by A7, A8; :: thesis: for a being Element of F_{2}() holds TVt . a = F_{4}(t,a)

let a be Element of F_{2}(); :: thesis: TVt . a = F_{4}(t,a)

thus TVt . a = F_{4}(t,a)
by A3, A8; :: thesis: verum

end;( TVt = f9 . (root-tree t) & ( for a being Element of F

consider TVt being Function such that

A8: TV . t = TVt and

A9: ( dom TVt = F

reconsider TVt = TVt as Function of F

take TVt = TVt; :: thesis: ( TVt = f9 . (root-tree t) & ( for a being Element of F

thus TVt = f9 . (root-tree t) by A7, A8; :: thesis: for a being Element of F

let a be Element of F

thus TVt . a = F

for rtl, rtr being Symbol of F

ex g, f1, f2 being Function of F

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F

let t1, t2 be Element of TS F

ex g, f1, f2 being Function of F

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F

let rtl, rtr be Symbol of F

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F

assume A10: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: ex g, f1, f2 being Function of F

( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F

ex f2 being Function st

( f . t2 = f2 & dom f2 = F

then reconsider f2 = f . t2 as Function of F

ex f1 being Function st

( f . t1 = f1 & dom f1 = F

then reconsider f1 = f . t1 as Function of F

NTV . [nt,(f . t1),(f . t2)] in FAB ;

then consider ntvval being Function such that

A11: ntvval = NTV . [nt,f1,f2] and

A12: ( dom ntvval = F

reconsider ntvval = ntvval as Function of F

take ntvval ; :: thesis: ex f1, f2 being Function of F

( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F

take f1 ; :: thesis: ex f2 being Function of F

( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F

take f2 ; :: thesis: ( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F

thus ( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 ) by A7, A10, A11; :: thesis: for a being Element of F

thus for a being Element of F