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

A1: now

let x be set ; :: thesis: ( x in dom (s +* (Initialized I)) implies (s +* (Initialized I)) . b₁ = ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . b₁ )
I c= Initialized I by SCMFSA6A:26;
then A2: dom I c= dom (Initialized I) by GRFUNC_1:8;
assume A3: x in dom (s +* (Initialized I)) ; :: thesis: (s +* (Initialized I)) . b₁ = ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . b₁

per cases ( x = intloc 0 or x = IC SCM+FSA or x in dom I or ( x is Element of NAT & not x in dom I ) or x is FinSeq-Location or ( x is Int-Location & x <> intloc 0 ) ) by A3, SCMFSA6A:35;

suppose A4: x = intloc 0 ; :: thesis: (s +* (Initialized I)) . b₁ = ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . b₁

then A5: not x in dom (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA6B:12;
x in dom (Initialized I) by A4, SCMFSA6A:45;
hence (s +* (Initialized I)) . x = (Initialized I) . x by FUNCT_4:14
.= 1 by A4, SCMFSA6A:46
.= (Initialized s) . x by A4, SCMFSA6C:3
.= ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . x by A5, FUNCT_4:12 ;
:: thesis: verum

end;

suppose A6: x = IC SCM+FSA ; :: thesis: (s +* (Initialized I)) . b₁ = ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . b₁

then A7: x in dom (I +* (Start-At 0 ,SCM+FSA )) by SF_MASTR:65;
x in dom (Initialized I) by A6, SCMFSA6A:24;
hence (s +* (Initialized I)) . x = (Initialized I) . x by FUNCT_4:14
.= 0 by A6, SCMFSA6A:46
.= (I +* (Start-At 0 ,SCM+FSA )) . x by A6, SF_MASTR:66
.= ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . x by A7, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A8: x in dom I ; :: thesis: (s +* (Initialized I)) . b₁ = ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . b₁

then x in (dom I) \/ (dom (Start-At 0 ,SCM+FSA )) by XBOOLE_0:def 3;
then A9: x in dom (I +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:def 1;
thus (s +* (Initialized I)) . x = (Initialized I) . x by A2, A8, FUNCT_4:14
.= I . x by A8, SCMFSA6A:50
.= (I +* (Start-At 0 ,SCM+FSA )) . x by A8, SCMFSA6B:7
.= ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . x by A9, FUNCT_4:14 ; :: thesis: verum

end;

suppose A10: ( x is Element of NAT & not x in dom I ) ; :: thesis: (s +* (Initialized I)) . b₁ = ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . b₁

then not x = IC SCM+FSA by COMPOS_1:3;
then not x in {(IC SCM+FSA )} by TARSKI:def 1;
then not x in (dom I) \/ {(IC SCM+FSA )} by A10, XBOOLE_0:def 3;
then not x in (dom I) \/ (dom (Start-At 0 ,SCM+FSA )) by FUNCOP_1:19;
then A11: not x in dom (I +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:def 1;
x <> IC SCM+FSA by A10, COMPOS_1:3;
then not x in dom (Initialized I) by A10, SCMFSA6A:44, SCMFSA_2:84;
hence (s +* (Initialized I)) . x = s . x by FUNCT_4:12
.= (Initialized s) . x by A10, SCMFSA6C:3
.= ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . x by A11, FUNCT_4:12 ;
:: thesis: verum

end;

suppose A12: x is FinSeq-Location ; :: thesis: (s +* (Initialized I)) . b₁ = ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . b₁

then not x = IC SCM+FSA by SCMFSA_2:82;
then A13: not x in {(IC SCM+FSA )} by TARSKI:def 1;
not x in dom I by A2, A12, SCMFSA6A:49;
then not x in (dom I) \/ {(IC SCM+FSA )} by A13, XBOOLE_0:def 3;
then not x in (dom I) \/ (dom (Start-At 0 ,SCM+FSA )) by FUNCOP_1:19;
then A14: not x in dom (I +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:def 1;
not x in dom (Initialized I) by A12, SCMFSA6A:49;
hence (s +* (Initialized I)) . x = s . x by FUNCT_4:12
.= (Initialized s) . x by A12, SCMFSA6C:3
.= ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . x by A14, FUNCT_4:12 ;
:: thesis: verum

end;

suppose A15: ( x is Int-Location & x <> intloc 0 ) ; :: thesis: (s +* (Initialized I)) . b₁ = ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . b₁

then not x = IC SCM+FSA by SCMFSA_2:81;
then A16: not x in {(IC SCM+FSA )} by TARSKI:def 1;
not x in dom I by A2, A15, SCMFSA6A:48;
then not x in (dom I) \/ {(IC SCM+FSA )} by A16, XBOOLE_0:def 3;
then not x in (dom I) \/ (dom (Start-At 0 ,SCM+FSA )) by FUNCOP_1:19;
then A17: not x in dom (I +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:def 1;
A18: x is read-write Int-Location by A15, SF_MASTR:def 5;
not x in dom (Initialized I) by A15, SCMFSA6A:48;
hence (s +* (Initialized I)) . x = s . x by FUNCT_4:12
.= (Initialized s) . x by A18, SCMFSA6C:3
.= ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) . x by A17, FUNCT_4:12 ;
:: thesis: verum

end;

end;

end;

dom (s +* (Initialized I)) = the carrier of SCM+FSA by PARTFUN1:def 4
.= dom ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) by PARTFUN1:def 4 ;
hence s +* (Initialized I) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by A1, FUNCT_1:9; :: thesis: verum