let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) holds
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
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 Initialized s,p & Ig is_halting_on Initialized s,p ) ) holds
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
let Ig be good Program of SCM+FSA; :: thesis: ( ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) implies DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s)) )
set I = Ig;
set IE = IExec (Ig,p,s);
assume A1: ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) ; :: thesis: DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))
A2: Ig is_halting_on Initialized s,p by A1, SCMFSA7B:25;
A3: Ig is_closed_on Initialized s,p by A1, SCMFSA7B:24;

now

A4: dom (Initialized (IExec (Ig,p,s))) = the carrier of SCM+FSA by PARTFUN1:def 4;
A5: dom (Initialized (IExec (Ig,p,s))) = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172
.= (Data-Locations SCM+FSA) \/ ({(IC )} \/ NAT) by XBOOLE_1:4 ;
A6: dom (IExec (Ig,p,s)) = the carrier of SCM+FSA by PARTFUN1:def 4;
hence dom (DataPart (Initialized (IExec (Ig,p,s)))) = (dom (IExec (Ig,p,s))) /\ (Data-Locations SCM+FSA) by A4, RELAT_1:90; :: thesis: for x being set st x in dom (DataPart (Initialized (IExec (Ig,p,s)))) holds
(DataPart (Initialized (IExec (Ig,p,s)))) . b₂ = (IExec (Ig,p,s)) . b₂
then A7: dom (DataPart (Initialized (IExec (Ig,p,s)))) = Data-Locations SCM+FSA by A4, A6, A5, XBOOLE_1:21;
let x be set ; :: thesis: ( x in dom (DataPart (Initialized (IExec (Ig,p,s)))) implies (DataPart (Initialized (IExec (Ig,p,s)))) . b₁ = (IExec (Ig,p,s)) . b₁ )
assume A8: x in dom (DataPart (Initialized (IExec (Ig,p,s)))) ; :: thesis: (DataPart (Initialized (IExec (Ig,p,s)))) . b₁ = (IExec (Ig,p,s)) . b₁

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A8, A7, SCMFSA_2:127, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: (DataPart (Initialized (IExec (Ig,p,s)))) . b₁ = (IExec (Ig,p,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 A9: not x9 is read-only ; :: thesis: (DataPart (Initialized (IExec (Ig,p,s)))) . x = (IExec (Ig,p,s)) . x

thus (DataPart (Initialized (IExec (Ig,p,s)))) . x = (Initialized (IExec (Ig,p,s))) . x by A8, A7, FUNCT_1:72
.= (IExec (Ig,p,s)) . x by A9, SCMFSA6C:3 ; :: thesis: verum

end;

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

then A10: x9 = intloc 0 by SF_MASTR:def 5;
thus (DataPart (Initialized (IExec (Ig,p,s)))) . x = (Initialized (IExec (Ig,p,s))) . x9 by A8, A7, FUNCT_1:72
.= 1 by A10, SCMFSA6C:3
.= (IExec (Ig,p,s)) . x by A3, A2, A10, SCMFSA8C:96 ; :: thesis: verum

end;

end;

end;

end;

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

then reconsider x9 = x as FinSeq-Location by SCMFSA_2:12;
thus (DataPart (Initialized (IExec (Ig,p,s)))) . x = (Initialized (IExec (Ig,p,s))) . x9 by A8, A7, FUNCT_1:72
.= (IExec (Ig,p,s)) . x by SCMFSA6C:3 ; :: thesis: verum

end;

end;

end;

hence DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s)) by FUNCT_1:68; :: thesis: verum