theorem Th3: :: SCM_1:3

for I1, I2 being Instruction of SCM
for F being NAT -defined the InstructionsF of SCM -valued total Function st <%I1%> ^ <%I2%> c= F holds
( F . 0 = I1 & F . 1 = I2 )