let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 )))
let I be Program of SCM+FSA ; :: thesis: s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 )))
A1: dom (s +* (Initialized I)) = the carrier of SCM+FSA by AMI_1:79
.= dom ((Initialize s) +* (I +* (Start-At (insloc 0 )))) by AMI_1:79 ;

now

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

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

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

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

end;

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

then A7: x in dom (I +* (Start-At (insloc 0 ))) 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
.= insloc 0 by A6, SCMFSA6A:46
.= (I +* (Start-At (insloc 0 ))) . x by A6, SF_MASTR:66
.= ((Initialize s) +* (I +* (Start-At (insloc 0 )))) . x by A7, FUNCT_4:14 ;
:: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

hence s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by A1, FUNCT_1:9; :: thesis: verum