let a, b be Int-Location; :: thesis: for s being State of SCM+FSA holds
( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )
let s be State of SCM+FSA; :: thesis: ( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )
consider A, B being Data-Location such that
A1: a = A and
A2: b = B and
A3: a := b = A := B by Def8;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A4: Exec ((a := b),s) = s +* (Exec ((A := B),S)) by A3, Th51;
hence (Exec ((a := b),s)) . (IC ) = (Exec ((A := B),S)) . (IC ) by Th53
.= succ (IC S) by AMI_3:2
.= succ (IC s) by Th62 ;
:: thesis: ( (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )
thus (Exec ((a := b),s)) . a = (Exec ((A := B),S)) . A by A1, A4, Th54
.= S . B by AMI_3:2
.= s . b by A2, Th55 ; :: thesis: ( ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )

hereby :: thesis: for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f

let c be Int-Location; :: thesis: ( c <> a implies (Exec ((a := b),s)) . c = s . c )
assume A5: c <> a ; :: thesis: (Exec ((a := b),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((a := b),s)) . c = (Exec ((A := B),S)) . C by A4, Th54
.= S . C by A1, A5, AMI_3:2
.= s . c by Th55 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (Exec ((a := b),s)) . f = s . f
A6: not f in dom (Exec ((A := B),S)) by Th44;
thus (Exec ((a := b),s)) . f = s . f by A4, A6, FUNCT_4:11; :: thesis: verum