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 (insloc n))) = (s +* (((intloc i) .--> m) +* (Start-At (insloc n)))) +* 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 (insloc n))) = (s +* (((intloc i) .--> m) +* (Start-At (insloc n)))) +* I
let i, m, n be Element of NAT ; :: thesis: (s +* I) +* (((intloc i) .--> m) +* (Start-At (insloc n))) = (s +* (((intloc i) .--> m) +* (Start-At (insloc n)))) +* I
set iS = ((intloc i) .--> m) +* (Start-At (insloc n));
A1: dom I misses dom (((intloc i) .--> m) +* (Start-At (insloc n))) by Th2;
then I +* (((intloc i) .--> m) +* (Start-At (insloc n))) = I \/ (((intloc i) .--> m) +* (Start-At (insloc n))) by FUNCT_4:32
.= (((intloc i) .--> m) +* (Start-At (insloc n))) +* I by A1, FUNCT_4:32 ;
hence (s +* I) +* (((intloc i) .--> m) +* (Start-At (insloc n))) = s +* ((((intloc i) .--> m) +* (Start-At (insloc n))) +* I) by FUNCT_4:15
.= (s +* (((intloc i) .--> m) +* (Start-At (insloc n)))) +* I by FUNCT_4:15 ;
:: thesis: verum