IC (SCM S) = IC SCM by AMI_3:4, SCMRING2:9;
then A1: ( 0. S <> 1_ S & dl. (S,0) <> IC (SCM S) ) by AMI_3:57, LMOD_6:def 2;
consider w being State of (SCM S);
set t = w +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)));
A2: InsCode (MultBy (p,q)) = 4 by RECDEF_2:def 1
.= InsCode (MultBy ((dl. (S,0)),(dl. (S,1)))) by RECDEF_2:def 1 ;
A3: dom (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) = {(dl. (S,0)),(dl. (S,1))} by FUNCT_4:65;
then dl. (S,0) in dom (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) by TARSKI:def 2;
then A4: (w +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,0)) = (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) . (dl. (S,0)) by FUNCT_4:14
.= 1_ S by AMI_3:52, FUNCT_4:66 ;
dl. (S,1) in dom (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) by A3, TARSKI:def 2;
then A5: (w +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,1)) = (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S))) . (dl. (S,1)) by FUNCT_4:14
.= 0. S by FUNCT_4:66 ;
dl. (S,0) in Data-Locations SCM by SCMRING2:1;
then XX: dl. (S,0) in Data-Locations (SCM S) by SCMRING2:31;
(Exec ((MultBy ((dl. (S,0)),(dl. (S,1)))),(w +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))))) . (dl. (S,0)) = ((w +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,0))) * ((w +* (((dl. (S,0)),(dl. (S,1))) --> ((1_ S),(0. S)))) . (dl. (S,1))) by SCMRING2:16
.= 0. S by A5, VECTSP_1:36 ;
hence for b₁ being InsType of (SCM S) st b₁ = InsCode (MultBy (p,q)) holds
not b₁ is jump-only by A2, A1, A4, AMISTD_1:def 3, XX; :: thesis: verum