let t be Terminal of SCM-AE; :: thesis: for n being Element of NAT holds SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%>
let n be Element of NAT ; :: thesis: SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%>
consider g being sequence of ( the InstructionsF of SCM ^omega) such that
A1: g = SCM-Compile . (root-tree t) and
A2: for n being Nat holds g . n = <%((dl. n) := (@ t))%> by Def11;
thus SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%> by A1, A2; :: thesis: verum