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