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 Def11k;
thus SCM-Compile (root-tree t),n = <%((dl. n) := (@ t))%> by A1, A2; :: thesis: verum