let R be Ring; :: thesis: for I being Instruction of (SCM R) st InsCode I = 4 holds

ex a, b being Data-Location of R st I = MultBy (a,b)

let I be Instruction of (SCM R); :: thesis: ( InsCode I = 4 implies ex a, b being Data-Location of R st I = MultBy (a,b) )

A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Nat st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;

assume InsCode I = 4 ; :: thesis: ex a, b being Data-Location of R st I = MultBy (a,b)

hence ex a, b being Data-Location of R st I = MultBy (a,b) by A1; :: thesis: verum

ex a, b being Data-Location of R st I = MultBy (a,b)

let I be Instruction of (SCM R); :: thesis: ( InsCode I = 4 implies ex a, b being Data-Location of R st I = MultBy (a,b) )

A1: ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Nat st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;

assume InsCode I = 4 ; :: thesis: ex a, b being Data-Location of R st I = MultBy (a,b)

hence ex a, b being Data-Location of R st I = MultBy (a,b) by A1; :: thesis: verum