let R be non trivial Ring; :: thesis: for a being Data-Location of R

for loc being Nat

for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a

let a be Data-Location of R; :: thesis: for loc being Nat

for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a

let loc be Nat; :: thesis: for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a

let s be State of (SCM R); :: thesis: s . a = (s +* (Start-At (loc,(SCM R)))) . a

a in the carrier of (SCM R) ;

then a in dom s by PARTFUN1:def 2;

then A1: ( dom (Start-At (loc,(SCM R))) = {(IC )} & a in (dom s) \/ (dom (Start-At (loc,(SCM R)))) ) by XBOOLE_0:def 3;

a <> IC by SCMRING3:2;

then not a in {(IC )} by TARSKI:def 1;

hence s . a = (s +* (Start-At (loc,(SCM R)))) . a by A1, FUNCT_4:def 1; :: thesis: verum

for loc being Nat

for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a

let a be Data-Location of R; :: thesis: for loc being Nat

for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a

let loc be Nat; :: thesis: for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a

let s be State of (SCM R); :: thesis: s . a = (s +* (Start-At (loc,(SCM R)))) . a

a in the carrier of (SCM R) ;

then a in dom s by PARTFUN1:def 2;

then A1: ( dom (Start-At (loc,(SCM R))) = {(IC )} & a in (dom s) \/ (dom (Start-At (loc,(SCM R)))) ) by XBOOLE_0:def 3;

a <> IC by SCMRING3:2;

then not a in {(IC )} by TARSKI:def 1;

hence s . a = (s +* (Start-At (loc,(SCM R)))) . a by A1, FUNCT_4:def 1; :: thesis: verum