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 Function of NAT,( the Instructions of SCM ^omega) such that
A1: g = SCM-Compile . (root-tree t) and
A2: for n being Element of NAT holds g . n = <%((dl. n) := (@ t))%> by Def13;
thus SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%> by A1, A2; :: thesis: verum