deffunc H₂( 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) = H₂(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) = H₁(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:35;
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:35;
hence ( xl = f . tl & xr = f . tr implies f . (nt -tree tl,tr) = nt -Meaning_on xl,xr ) by A1, A2; :: thesis: verum