let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds DataPart (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) = DataPart (IExec (I,s))
let I be Program of SCM+FSA; :: thesis: DataPart (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) = DataPart (IExec (I,s))
set s1 = s +* (Initialized I);
A1: IExec (I,s) = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT) by SCMFSA6B:def 1;

A2: now

let f be FinSeq-Location ; :: thesis: (IExec (I,s)) . f = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . f
( f in dom (s | NAT) implies f is Element of NAT ) by RELAT_1:86;
hence (IExec (I,s)) . f = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . f by A1, FUNCT_4:12, SCMFSA_2:85; :: thesis: verum

end;

now

let b be Int-Location ; :: thesis: (IExec (I,s)) . b = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . b
( b in dom (s | NAT) implies b is Element of NAT ) by RELAT_1:86;
hence (IExec (I,s)) . b = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . b by A1, FUNCT_4:12, SCMFSA_2:84; :: thesis: verum

end;

hence DataPart (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) = DataPart (IExec (I,s)) by A2, SCMFSA6A:38; :: thesis: verum