set IF = Int-Locations \/ FinSeq-Locations ;
let I be InitHalting keepInt0_1 Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA holds DataPart (Initialized (IExec I,s)) = DataPart (IExec I,s)
let s be State of SCM+FSA ; :: thesis: DataPart (Initialized (IExec I,s)) = DataPart (IExec I,s)
set IE = IExec I,s;

now

A1: dom (Initialized (IExec I,s)) = the carrier of SCM+FSA by PARTFUN1:def 4;
then A2: dom (Initialized (IExec I,s)) = (Int-Locations \/ FinSeq-Locations ) \/ ({(IC SCM+FSA )} \/ NAT ) by SCMFSA_2:8, XBOOLE_1:4;
A3: dom (IExec I,s) = the carrier of SCM+FSA by PARTFUN1:def 4;
hence dom (DataPart (Initialized (IExec I,s))) = (dom (IExec I,s)) /\ (Int-Locations \/ FinSeq-Locations ) by A1, RELAT_1:90, SCMFSA_2:127; :: thesis: for x being set st x in dom (DataPart (Initialized (IExec I,s))) holds
(DataPart (Initialized (IExec I,s))) . b₂ = (IExec I,s) . b₂
then A4: dom (DataPart (Initialized (IExec I,s))) = Int-Locations \/ FinSeq-Locations by A1, A3, A2, XBOOLE_1:21;
let x be set ; :: thesis: ( x in dom (DataPart (Initialized (IExec I,s))) implies (DataPart (Initialized (IExec I,s))) . b₁ = (IExec I,s) . b₁ )
assume A5: x in dom (DataPart (Initialized (IExec I,s))) ; :: thesis: (DataPart (Initialized (IExec I,s))) . b₁ = (IExec I,s) . b₁

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A5, A4, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: (DataPart (Initialized (IExec I,s))) . b₁ = (IExec I,s) . b₁

then reconsider x9 = x as Int-Location by SCMFSA_2:11;

hereby :: thesis: verum

per cases ( not x9 is read-only or x9 is read-only ) ;

suppose A6: not x9 is read-only ; :: thesis: (DataPart (Initialized (IExec I,s))) . x = (IExec I,s) . x

thus (DataPart (Initialized (IExec I,s))) . x = (Initialized (IExec I,s)) . x by A5, A4, FUNCT_1:72, SCMFSA_2:127
.= (IExec I,s) . x by A6, SCMFSA6C:3 ; :: thesis: verum

end;

suppose x9 is read-only ; :: thesis: (DataPart (Initialized (IExec I,s))) . x = (IExec I,s) . x

then A7: x9 = intloc 0 by SF_MASTR:def 5;
thus (DataPart (Initialized (IExec I,s))) . x = (Initialized (IExec I,s)) . x9 by A5, A4, FUNCT_1:72, SCMFSA_2:127
.= 1 by A7, SCMFSA6C:3
.= (IExec I,s) . x by A7, Th17 ; :: thesis: verum

end;

end;

end;

end;

suppose x in FinSeq-Locations ; :: thesis: (DataPart (Initialized (IExec I,s))) . b₁ = (IExec I,s) . b₁

then reconsider x9 = x as FinSeq-Location by SCMFSA_2:12;
thus (DataPart (Initialized (IExec I,s))) . x = (Initialized (IExec I,s)) . x9 by A5, A4, FUNCT_1:72, SCMFSA_2:127
.= (IExec I,s) . x by SCMFSA6C:3 ; :: thesis: verum

end;

end;

end;

hence DataPart (Initialized (IExec I,s)) = DataPart (IExec I,s) by FUNCT_1:68, SCMFSA_2:127; :: thesis: verum