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