deffunc H2( Terminal of SCM-AE) -> Element of INT = (id INT) . (s . $1);
let it1, it2 be Integer; :: thesis: ( ex f being Function of (TS SCM-AE),INT st
( it1 = 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) ) ) & ex f being Function of (TS SCM-AE),INT st
( it2 = 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) ) ) implies it1 = it2 )
given f1 being Function of (TS SCM-AE),INT such that A3: it1 = f1 . term and
A4: for t being Terminal of SCM-AE holds f1 . (root-tree t) = s . t and
A5: 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 = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ; :: thesis: ( for f being Function of (TS SCM-AE),INT holds
( not it2 = f . term or ex t being Terminal of SCM-AE st not f . (root-tree t) = s . t or ex nt being NonTerminal of SCM-AE ex tl, tr being bin-term ex rtl, rtr being Symbol of SCM-AE st
( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> & ex xl, xr being Element of INT st
( xl = f . tl & xr = f . tr & not f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) ) or it1 = it2 )
A6: now :: thesis: ( ( for t being Terminal of SCM-AE holds f1 . (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 = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,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 = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let t be Terminal of SCM-AE; :: thesis: f1 . (root-tree t) = H2(t)
s . t in INT by INT_1:def 2;
then (id INT) . (s . t) = s . t by FUNCT_1:18;
hence f1 . (root-tree t) = H2(t) by A4; :: 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 = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,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 = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,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 = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) )
assume A7: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of INT st xl = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let xl, xr be Element of INT ; :: thesis: ( xl = f1 . tl & xr = f1 . tr implies f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) )
assume A8: ( xl = f1 . tl & xr = f1 . tr ) ; :: thesis: f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,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 f1 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) by A5, A7, A8; :: thesis: verum
end;
given f2 being Function of (TS SCM-AE),INT such that A9: it2 = f2 . term and
A10: for t being Terminal of SCM-AE holds f2 . (root-tree t) = s . t and
A11: 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 = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ; :: thesis: it1 = it2
A12: now :: thesis: ( ( for t being Terminal of SCM-AE holds f2 . (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 = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,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 = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let t be Terminal of SCM-AE; :: thesis: f2 . (root-tree t) = H2(t)
s . t in INT by INT_1:def 2;
then (id INT) . (s . t) = s . t by FUNCT_1:18;
hence f2 . (root-tree t) = H2(t) by A10; :: 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 = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,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 = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,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 = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) )
assume A13: ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of INT st xl = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr)
let xl, xr be Element of INT ; :: thesis: ( xl = f2 . tl & xr = f2 . tr implies f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) )
assume A14: ( xl = f2 . tl & xr = f2 . tr ) ; :: thesis: f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,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 f2 . (nt -tree (tl,tr)) = H1(nt,rtl,rtr,xl,xr) by A11, A13, A14; :: thesis: verum
end;
f1 = f2 from BINTREE1:sch 4(A6, A12);
 hence it1 = it2 by A3, A9; :: thesis: verum