let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds (Initialized s) +* (Initialized I) = s +* (Initialized I)
let I be Program of SCM+FSA; :: thesis: (Initialized s) +* (Initialized I) = s +* (Initialized I)
A1: dom I misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;

now

let x be set ; :: thesis: ( x in dom ((intloc 0) .--> 1) implies not x in dom I )
A2: dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:19;
assume x in dom ((intloc 0) .--> 1) ; :: thesis: not x in dom I
then x = intloc 0 by A2, TARSKI:def 1;
hence not x in dom I by SCMFSA6A:47; :: thesis: verum

end;

then A3: dom I misses dom ((intloc 0) .--> 1) by XBOOLE_0:3;
thus (Initialized s) +* (Initialized I) = ((s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) +* (Initialized I)
.= ((s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) by FUNCT_4:15
.= (((s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) +* I) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= ((s +* ((intloc 0) .--> 1)) +* ((Start-At (0,SCM+FSA)) +* I)) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= ((s +* ((intloc 0) .--> 1)) +* (I +* (Start-At (0,SCM+FSA)))) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by A1, FUNCT_4:36
.= (((s +* ((intloc 0) .--> 1)) +* I) +* (Start-At (0,SCM+FSA))) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= ((s +* (((intloc 0) .--> 1) +* I)) +* (Start-At (0,SCM+FSA))) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= ((s +* (I +* ((intloc 0) .--> 1))) +* (Start-At (0,SCM+FSA))) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by A3, FUNCT_4:36
.= (((s +* I) +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= ((s +* I) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= (s +* I) +* ((((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) by FUNCT_4:15
.= ((s +* I) +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) by FUNCT_4:15
.= (s +* (I +* ((intloc 0) .--> 1))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:15
.= s +* (Initialized I) by FUNCT_4:15 ; :: thesis: verum