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;
A4: Initialized I = Initialize (I +* ((intloc 0) .--> 1)) by FUNCT_4:15;
thus (Initialized s) +* (Initialized I) = (Initialize (s +* ((intloc 0) .--> 1))) +* (I +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15
.= ((Initialize (s +* ((intloc 0) .--> 1))) +* I) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= ((s +* ((intloc 0) .--> 1)) +* ((Start-At (0,SCM+FSA)) +* I)) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= ((s +* ((intloc 0) .--> 1)) +* (Initialize I)) +* (Initialize ((intloc 0) .--> 1)) by A1, FUNCT_4:36
.= (Initialize ((s +* ((intloc 0) .--> 1)) +* I)) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= (Initialize (s +* (((intloc 0) .--> 1) +* I))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= (Initialize (s +* (I +* ((intloc 0) .--> 1)))) +* (Initialize ((intloc 0) .--> 1)) by A3, FUNCT_4:36
.= (Initialize ((s +* I) +* ((intloc 0) .--> 1))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= ((s +* I) +* (Initialize ((intloc 0) .--> 1))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= (s +* I) +* ((Initialize ((intloc 0) .--> 1)) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15
.= Initialize ((s +* I) +* ((intloc 0) .--> 1)) by FUNCT_4:15
.= Initialize (s +* (I +* ((intloc 0) .--> 1))) by FUNCT_4:15
.= s +* (Initialized I) by FUNCT_4:15, A4 ; :: thesis: verum