let A be Data-Location ; :: thesis: for a being Int-Location
for S being State of SCM
for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a
let a be Int-Location ; :: thesis: for S being State of SCM
for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a
let S be State of SCM; :: thesis: for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a
let s1, s be State of SCM+FSA; :: thesis: ( s1 = s +* S & A = a implies S . A = s1 . a )
assume that
A1: s1 = s +* S and
A2: A = a ; :: thesis: S . A = s1 . a
A3: dom S = SCM-Memory by PARTFUN1:def 2;
thus s1 . a = (s +* S) . a by A1
.= S . A by A2, A3, FUNCT_4:13 ; :: thesis: verum