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