let A be Data-Location; :: thesis: for a being Int-Location
for S being State of SCM
for s, s1 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 s, s1 being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a
let S be State of SCM; :: thesis: for s, s1 being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a
let s, s1 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
dom S = SCM-Memory by PARTFUN1:def 2;
hence s1 . a = S . A by A1, A2, FUNCT_4:13; :: thesis: verum