let F be NAT -defined the InstructionsF of SCM -valued total Function; for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM st (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%> c= F holds
( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 )
let I1, I2, I3, I4, I5, I6, I7, I8, I9 be Instruction of SCM; ( (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%> c= F implies ( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 ) )
assume A1:
(((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%> c= F
; ( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 )
set I = (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>;
A2:
( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 2 = I3 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 3 = I4 )
by AFINSQ_1:50;
A3:
( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 6 = I7 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 7 = I8 )
by AFINSQ_1:50;
A4:
( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 4 = I5 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 5 = I6 )
by AFINSQ_1:50;
A5:
( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 8 = I9 & len ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) = 9 )
by AFINSQ_1:50;
len ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) = 9
by AFINSQ_1:50;
then A6:
( 0 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 1 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 2 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 3 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 4 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 5 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 6 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 7 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) & 8 in dom ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) )
by CARD_1:57, ENUMSET1:def 7;
( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 0 = I1 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 1 = I2 )
by AFINSQ_1:50;
hence
( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 )
by A2, A4, A3, A5, A6, A1, GRFUNC_1:2; verum