let f1, f2 be Function of (TS SCM-AE ),(Funcs NAT ,(the Instructions of SCM ^omega )); :: thesis: ( ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & f1 = f1 . t1 & f2 = f1 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) & ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & f1 = f2 . t1 & f2 = f2 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) implies f1 = f2 )
assume that
A3: ( ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = ((g1 . n) ^ (g2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) and
A5: ( ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = ((g1 . n) ^ (g2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) ; :: thesis: f1 = f2
B3: ( ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) ) ) )

proof

thus for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) ) :: thesis: for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )

proof

let t be Terminal of SCM-AE ; :: thesis: ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) )
consider g being Function of NAT ,(the Instructions of SCM ^omega ) such that
W: ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) by A3;
take g ; :: thesis: ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) )
thus ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) ) by W; :: thesis: verum

end;

thus for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) ) :: thesis: verum

proof

let nt be NonTerminal of SCM-AE ; :: thesis: for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
let t1, t2 be bin-term; :: thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
let rtl, rtr be Symbol of SCM-AE ; :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) ) )
assume Z: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
consider g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) such that
W: ( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = ((g1 . n) ^ (g2 . (n + 1))) ^ (Selfwork nt,n) ) ) by A3, Z;
take g ; :: thesis: ex g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
take g1 ; :: thesis: ex g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
take g2 ; :: thesis: ( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
thus ( g = f1 . (nt -tree t1,t2) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) ) by W; :: thesis: verum

end;

end;

B5: ( ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) ) ) )

proof

thus for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) ) :: thesis: for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )

proof

let t be Terminal of SCM-AE ; :: thesis: ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) )
consider g being Function of NAT ,(the Instructions of SCM ^omega ) such that
W: ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> ) ) by A5;
take g ; :: thesis: ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) )
thus ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H₃(t,n) ) ) by W; :: thesis: verum

end;

thus for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) ) :: thesis: verum

proof

let nt be NonTerminal of SCM-AE ; :: thesis: for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
let t1, t2 be bin-term; :: thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
let rtl, rtr be Symbol of SCM-AE ; :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) ) )
assume Z: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: ex g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
consider g, g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) such that
W: ( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = ((g1 . n) ^ (g2 . (n + 1))) ^ (Selfwork nt,n) ) ) by A5, Z;
take g ; :: thesis: ex g1, g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
take g1 ; :: thesis: ex g2 being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
take g2 ; :: thesis: ( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) )
thus ( g = f2 . (nt -tree t1,t2) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H₂(nt,g1,g2,n) ) ) by W; :: thesis: verum

end;

end;

thus f1 = f2 from BINTREE1:sch 6(B3, B5); :: thesis: verum