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 SF_MASTR:64;

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) by SCMFSA6A:def 4
.= ((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