deffunc H2( Terminal of SCM-AE) -> Element of INT = (id INT) . (s . $1);
consider f being Function of (TS SCM-AE),INT such that
A1: ( ( for t being Terminal of SCM-AE holds f . (root-tree t) = H2(t) ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) ) ) from BINTREE1:sch 3();
 reconsider IT = f . term as Element of INT ;
take IT ; :: thesis: ex f being Function of (TS SCM-AE),INT st
( IT = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) )
take f ; :: thesis: ( IT = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) )
thus IT = f . term ; :: thesis: ( ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) )
hereby :: thesis: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr)
let t be Terminal of SCM-AE; :: thesis: f . (root-tree t) = s . t
s . t in INT by INT_1:def 2;
then (id INT) . (s . t) = s . t by FUNCT_1:18;
hence f . (root-tree t) = s . t by A1; :: thesis: verum
end;
let nt be NonTerminal of SCM-AE; :: thesis: for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr)
let tl, tr be bin-term; :: thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr)
let rtl, rtr be Symbol of SCM-AE; :: thesis: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) )
assume A2: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr)
let xl, xr be Element of INT ; :: thesis: ( xl = f . tl & xr = f . tr implies f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) )
nt -Meaning_on (xl,xr) in INT by INT_1:def 2;
then (id INT) . (nt -Meaning_on (xl,xr)) = nt -Meaning_on (xl,xr) by FUNCT_1:18;
hence ( xl = f . tl & xr = f . tr implies f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) by A1, A2; :: thesis: verum