set w = the State of (SCM S);
consider e being Element of S such that
A1: e <> 0. S by STRUCT_0:def 19;
reconsider e = e as Element of S ;

A2: now

assume - e = 0. S ; :: thesis: contradiction
then e = - (0. S) by RLVECT_1:30;
hence contradiction by A1, RLVECT_1:25; :: thesis: verum

end;

set t = the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e));
A3: InsCode (SubFrom (p,q)) = 3 by RECDEF_2:def 1
.= InsCode (SubFrom ((dl. (S,0)),(dl. (S,1)))) by RECDEF_2:def 1 ;
A4: dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) = {(dl. (S,0)),(dl. (S,1))} by FUNCT_4:65;
then dl. (S,0) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by TARSKI:def 2;
then A5: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,0)) = (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,0)) by FUNCT_4:14
.= 0. S by AMI_3:52, FUNCT_4:66 ;
dl. (S,1) in dom (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) by A4, TARSKI:def 2;
then A6: ( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1)) = (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e)) . (dl. (S,1)) by FUNCT_4:14
.= e by FUNCT_4:66 ;
dl. (S,0) in Data-Locations SCM by SCMRING2:1;
then A7: dl. (S,0) in Data-Locations (SCM S) by SCMRING2:31;
(Exec ((SubFrom ((dl. (S,0)),(dl. (S,1)))),( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))))) . (dl. (S,0)) = (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,0))) - (( the State of (SCM S) +* (((dl. (S,0)),(dl. (S,1))) --> ((0. S),e))) . (dl. (S,1))) by SCMRING2:15
.= - e by A5, A6, RLVECT_1:27 ;
hence for b₁ being InsType of (SCM S) st b₁ = InsCode (SubFrom (p,q)) holds
not b₁ is jump-only by A3, A5, A2, AMISTD_1:def 3, A7; :: thesis: verum