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