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 & ( for t being Terminal of SCM-AE holds f1 . (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 = 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 )

A4: now

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) = H₁(nt,rtl,rtr,xl,xr)

let t be Terminal of SCM-AE ; :: thesis: f1 . (root-tree t) = H₂(t)
s . t in INT by INT_1:def 2;
then (id INT ) . (s . t) = s . t by FUNCT_1:35;
hence f1 . (root-tree t) = H₂(t) by A3; :: 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) = H₁(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) = H₁(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) = H₁(nt,rtl,rtr,xl,xr) )
assume A5: ( 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) = H₁(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) = H₁(nt,rtl,rtr,xl,xr) )
assume A6: ( xl = f1 . tl & xr = f1 . tr ) ; :: thesis: f1 . (nt -tree tl,tr) = H₁(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:35;
hence f1 . (nt -tree tl,tr) = H₁(nt,rtl,rtr,xl,xr) by A3, A5, A6; :: thesis: verum

end;

given f2 being Function of TS SCM-AE , INT such that A7: ( it2 = f2 . term & ( for t being Terminal of SCM-AE holds f2 . (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 = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree tl,tr) = nt -Meaning_on xl,xr ) ) ; :: thesis: it1 = it2

A8: now

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) = H₁(nt,rtl,rtr,xl,xr)

let t be Terminal of SCM-AE ; :: thesis: f2 . (root-tree t) = H₂(t)
s . t in INT by INT_1:def 2;
then (id INT ) . (s . t) = s . t by FUNCT_1:35;
hence f2 . (root-tree t) = H₂(t) by A7; :: 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) = H₁(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) = H₁(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) = H₁(nt,rtl,rtr,xl,xr) )
assume A9: ( 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) = H₁(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) = H₁(nt,rtl,rtr,xl,xr) )
assume A10: ( xl = f2 . tl & xr = f2 . tr ) ; :: thesis: f2 . (nt -tree tl,tr) = H₁(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:35;
hence f2 . (nt -tree tl,tr) = H₁(nt,rtl,rtr,xl,xr) by A7, A9, A10; :: thesis: verum

end;

f1 = f2 from BINTREE1:sch 4(A4, A8);
hence it1 = it2 by A3, A7; :: thesis: verum