consider f being Function of (),(Funcs (NAT,())) such that
A1: ( ( for t being Terminal of SCM-AE ex g being sequence of () st
( g = f . () & ( for n being Element of NAT holds g . n = H3(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, f1, f2 being sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = H2(nt,f1,f2,n) ) ) ) ) from take f ; :: thesis: ( ( for t being Terminal of SCM-AE ex g being sequence of () st
( g = f . () & ( for n being 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 sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) )

( ( for t being Terminal of SCM-AE ex g being sequence of () st
( g = f . () & ( for n being 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 sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) )
proof
thus for t being Terminal of SCM-AE ex g being sequence of () st
( g = f . () & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) :: 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, f1, f2 being sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )
proof
let t be Terminal of SCM-AE; :: thesis: ex g being sequence of () st
( g = f . () & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) )

consider g being sequence of () such that
A2: g = f . () and
A3: for n being Element of NAT holds g . n = H3(t,n) by A1;
take g ; :: thesis: ( g = f . () & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) )
thus g = f . () by A2; :: thesis: for n being Nat holds g . n = <%((dl. n) := (@ t))%>
let n be Nat; :: thesis: g . n = <%((dl. n) := (@ t))%>
n in NAT by ORDINAL1:def 12;
then g . n = H3(t,n) by A3;
hence g . n = <%((dl. n) := (@ t))%> ; :: 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, f1, f2 being sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,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, f1, f2 being sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,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, f1, f2 being sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )

let rtl, rtr be Symbol of SCM-AE; :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, f1, f2 being sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) )

assume A4: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: ex g, f1, f2 being sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )

consider g, f1, f2 being sequence of () such that
A5: ( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 ) and
A6: for n being Element of NAT holds g . n = H2(nt,f1,f2,n) by A4, A1;
take g ; :: thesis: ex f1, f2 being sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )

take f1 ; :: thesis: ex f2 being sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )

take f2 ; :: thesis: ( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )
thus ( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 ) by A5; :: thesis: for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n))
let n be Nat; :: thesis: g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n))
g . n = H2(nt,f1,f2,n) by A6;
hence g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ; :: thesis: verum
end;
end;
hence ( ( for t being Terminal of SCM-AE ex g being sequence of () st
( g = f . () & ( for n being 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 sequence of () st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) ) ; :: thesis: verum