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

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