let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA
for i, m, n being Element of NAT holds (s +* I) +* (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) = (s +* (((intloc i) .--> m) +* (Start-At n,SCM+FSA ))) +* I
let s be State of SCM+FSA ; :: thesis: for i, m, n being Element of NAT holds (s +* I) +* (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) = (s +* (((intloc i) .--> m) +* (Start-At n,SCM+FSA ))) +* I
let i, m, n be Element of NAT ; :: thesis: (s +* I) +* (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) = (s +* (((intloc i) .--> m) +* (Start-At n,SCM+FSA ))) +* I
set iS = ((intloc i) .--> m) +* (Start-At n,SCM+FSA );
A1: dom I misses dom (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) by Th2;
then I +* (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) = I \/ (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) by FUNCT_4:32
.= (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) +* I by A1, FUNCT_4:32 ;
hence (s +* I) +* (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) = s +* ((((intloc i) .--> m) +* (Start-At n,SCM+FSA )) +* I) by FUNCT_4:15
.= (s +* (((intloc i) .--> m) +* (Start-At n,SCM+FSA ))) +* I by FUNCT_4:15 ;
:: thesis: verum