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 = F5($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 = F4($1,a);
reconsider FAB = Funcs (F2(),F3()) as non empty set ;
A1: 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( set ) -> Element of F3() = F4(x,$1);
consider y being Function of F2(),F3() such that
A2: for a being Element of F2() holds y . a = H1(a) from FUNCT_2:sch 4();
 ( 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 A2; :: thesis: verum
end;
consider TV being Function of (Terminals F1()),FAB such that
A3: for e being Element of Terminals F1() holds S2[e,TV . e] from FUNCT_2:sch 3(A1);
 deffunc H1( Terminal of F1()) -> Element of FAB = TV . $1;
A4: 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( set ) -> Element of F3() = F5(x,y,z,$1);
consider fab being Function of F2(),F3() such that
A5: for a being Element of F2() holds fab . a = H2(a) from FUNCT_2:sch 4();
 ( 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 A5; :: thesis: verum
end;
consider NTV being Function of [:(NonTerminals F1()),FAB,FAB:],FAB such that
A6: for x being Element of NonTerminals F1()
for y, z being Element of FAB holds S1[x,y,z,NTV . [x,y,z]] from MULTOP_1:sch 1(A4);
 deffunc H2( Element of NonTerminals F1(), set , set , Element of FAB, Element of FAB) -> Element of FAB = NTV . [$1,$4,$5];
consider f being Function of (TS F1()),FAB such that
A7: ( ( for t being Terminal of F1() holds f . (root-tree t) = 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 = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) ) from BINTREE1:sch 3();
 reconsider f9 = f as Function of (TS F1()),(Funcs (F2(),F3())) ;
take f9 ; :: thesis: ( ( for t being Terminal of F1() ex g being Function of F2(),F3() st
( g = f9 . (root-tree t) & ( for a being Element of F2() holds g . a = F4(t,a) ) ) ) & ( for nt being NonTerminal of F1()
for t1, t2 being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) ) )
hereby :: thesis: for nt being NonTerminal of F1()
for t1, t2 being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) )
let t be Terminal of F1(); :: thesis: ex TVt being Function of F2(),F3() st
( TVt = f9 . (root-tree t) & ( for a being Element of F2() holds TVt . a = F4(t,a) ) )
consider TVt being Function such that
A8: TV . t = TVt and
A9: ( dom TVt = F2() & rng TVt c= F3() ) by FUNCT_2:def 2;
reconsider TVt = TVt as Function of F2(),F3() by A9, FUNCT_2:def 1, RELSET_1:4;
take TVt = TVt; :: thesis: ( TVt = f9 . (root-tree t) & ( for a being Element of F2() holds TVt . a = F4(t,a) ) )
thus TVt = f9 . (root-tree t) by A7, A8; :: thesis: for a being Element of F2() holds TVt . a = F4(t,a)
let a be Element of F2(); :: thesis: TVt . a = F4(t,a)
thus TVt . a = F4(t,a) by A3, A8; :: thesis: verum
end;
let nt be NonTerminal of F1(); :: thesis: for t1, t2 being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) )
let t1, t2 be Element of TS F1(); :: thesis: for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) )
let rtl, rtr be Symbol of F1(); :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, f1, f2 being Function of F2(),F3() st
( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(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 F2(),F3() st
( g = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) )
ex f2 being Function st
( f . t2 = f2 & dom f2 = F2() & rng f2 c= F3() ) by FUNCT_2:def 2;
then reconsider f2 = f . t2 as Function of F2(),F3() by FUNCT_2:def 1, RELSET_1:4;
ex f1 being Function st
( f . t1 = f1 & dom f1 = F2() & rng f1 c= F3() ) by FUNCT_2:def 2;
then reconsider f1 = f . t1 as Function of F2(),F3() 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 = F2() & rng ntvval c= F3() ) by FUNCT_2:def 2;
reconsider ntvval = ntvval as Function of F2(),F3() by A12, FUNCT_2:def 1, RELSET_1:4;
take ntvval ; :: thesis: ex f1, f2 being Function of F2(),F3() st
( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds ntvval . a = F5(nt,f1,f2,a) ) )
take f1 ; :: thesis: ex f2 being Function of F2(),F3() st
( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds ntvval . a = F5(nt,f1,f2,a) ) )
take f2 ; :: thesis: ( ntvval = f9 . (nt -tree (t1,t2)) & f1 = f9 . t1 & f2 = f9 . t2 & ( for a being Element of F2() holds ntvval . a = F5(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 F2() holds ntvval . a = F5(nt,f1,f2,a)
thus for a being Element of F2() holds ntvval . a = F5(nt,f1,f2,a) by A6, A11; :: thesis: verum