let T be InsType of the InstructionsF of SCM; :: thesis: not not T = 0 & ... & not T = 8

consider y being object such that

A1: [T,y] in proj1 the InstructionsF of SCM by XTUPLE_0:def 12;

consider x being object such that

A2: [[T,y],x] in the InstructionsF of SCM by A1, XTUPLE_0:def 12;

reconsider I = [T,y,x] as Instruction of SCM by A2;

T = InsCode I ;

hence not not T = 0 & ... & not T = 8 by AMI_5:5; :: thesis: verum

consider y being object such that

A1: [T,y] in proj1 the InstructionsF of SCM by XTUPLE_0:def 12;

consider x being object such that

A2: [[T,y],x] in the InstructionsF of SCM by A1, XTUPLE_0:def 12;

reconsider I = [T,y,x] as Instruction of SCM by A2;

T = InsCode I ;

hence not not T = 0 & ... & not T = 8 by AMI_5:5; :: thesis: verum