let s be State of SCM+FSA; :: thesis: for f being FinSeq-Location
for a, b being Int-Location holds (Exec ((b := (f,a)),s)) . b = (s . f) /. |.(s . a).|
let f be FinSeq-Location ; :: thesis: for a, b being Int-Location holds (Exec ((b := (f,a)),s)) . b = (s . f) /. |.(s . a).|
let a, b be Int-Location; :: thesis: (Exec ((b := (f,a)),s)) . b = (s . f) /. |.(s . a).|
ex k being Nat st
( k = |.(s . a).| & (Exec ((b := (f,a)),s)) . b = (s . f) /. k ) by SCMFSA_2:72;
hence (Exec ((b := (f,a)),s)) . b = (s . f) /. |.(s . a).| ; :: thesis: verum