let s be State of SCM+FSA ; :: thesis: for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_closed_on Initialize s & Ig is_halting_on Initialize s ) ) holds
DataPart (Initialize (IExec Ig,s)) = DataPart (IExec Ig,s)
let Ig be good Program of SCM+FSA ; :: thesis: ( ( Ig is parahalting or ( Ig is_closed_on Initialize s & Ig is_halting_on Initialize s ) ) implies DataPart (Initialize (IExec Ig,s)) = DataPart (IExec Ig,s) )
set I = Ig;
assume A1: ( Ig is parahalting or ( Ig is_closed_on Initialize s & Ig is_halting_on Initialize s ) ) ; :: thesis: DataPart (Initialize (IExec Ig,s)) = DataPart (IExec Ig,s)
A2: ( Ig is_closed_on Initialize s & Ig is_halting_on Initialize s ) by A1, SCMFSA7B:24, SCMFSA7B:25;
set IE = IExec Ig,s;
set Ins = NAT ;

now

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

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

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

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

hereby :: thesis: verum

per cases ( not x' is read-only or x' is read-only ) ;

suppose A7: not x' is read-only ; :: thesis: (DataPart (Initialize (IExec Ig,s))) . x = (IExec Ig,s) . x

thus (DataPart (Initialize (IExec Ig,s))) . x = (Initialize (IExec Ig,s)) . x by A5, A6, FUNCT_1:72, SCMFSA_2:127
.= (IExec Ig,s) . x by A7, SCMFSA6C:3 ; :: thesis: verum

end;

suppose x' is read-only ; :: thesis: (DataPart (Initialize (IExec Ig,s))) . x = (IExec Ig,s) . x

then A8: x' = intloc 0 by SF_MASTR:def 5;
thus (DataPart (Initialize (IExec Ig,s))) . x = (Initialize (IExec Ig,s)) . x' by A5, A6, FUNCT_1:72, SCMFSA_2:127
.= 1 by A8, SCMFSA6C:3
.= (IExec Ig,s) . x by A2, A8, SCMFSA8C:96 ; :: thesis: verum

end;

end;

end;

end;

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

then reconsider x' = x as FinSeq-Location by SCMFSA_2:12;
thus (DataPart (Initialize (IExec Ig,s))) . x = (Initialize (IExec Ig,s)) . x' by A5, A6, FUNCT_1:72, SCMFSA_2:127
.= (IExec Ig,s) . x by SCMFSA6C:3 ; :: thesis: verum

end;

end;

end;

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