let I1, I2 be Instruction of SCM; :: thesis: for F being NAT -defined the InstructionsF of SCM -valued total Function st <%I1%> ^ <%I2%> c= F holds
( F . 0 = I1 & F . 1 = I2 )
let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: ( <%I1%> ^ <%I2%> c= F implies ( F . 0 = I1 & F . 1 = I2 ) )
assume A1: <%I1%> ^ <%I2%> c= F ; :: thesis: ( F . 0 = I1 & F . 1 = I2 )
set ins = <%I1%> ^ <%I2%>;
A2: <%I1%> ^ <%I2%> = <%I1,I2%> ;
then A3: (<%I1%> ^ <%I2%>) . 1 = I2 ;
A4: (<%I1%> ^ <%I2%>) . 0 = I1 by A2;
len (<%I1%> ^ <%I2%>) = 2 by A2, AFINSQ_1:38;
then ( 0 in dom (<%I1%> ^ <%I2%>) & 1 in dom (<%I1%> ^ <%I2%>) ) by CARD_1:50, TARSKI:def 2;
hence ( F . 0 = I1 & F . 1 = I2 ) by A1, A3, A4, GRFUNC_1:2; :: thesis: verum