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

A2: now

let b be Int-Location ; :: thesis: (IExec I,s) . b = (Result (s +* (Initialized I))) . b

now

assume b in dom (s | NAT ) ; :: thesis: b is Instruction-Location of SCM+FSA
then b in NAT by RELAT_1:86;
hence b is Instruction-Location of SCM+FSA by AMI_1:def 4; :: thesis: verum

end;

hence (IExec I,s) . b = (Result (s +* (Initialized I))) . b by A1, FUNCT_4:12, SCMFSA_2:84; :: thesis: verum

end;

now

let f be FinSeq-Location ; :: thesis: (IExec I,s) . f = (Result (s +* (Initialized I))) . f

now

assume f in dom (s | NAT ) ; :: thesis: f is Instruction-Location of SCM+FSA
then f in NAT by RELAT_1:86;
hence f is Instruction-Location of SCM+FSA by AMI_1:def 4; :: thesis: verum

end;

hence (IExec I,s) . f = (Result (s +* (Initialized I))) . f by A1, FUNCT_4:12, SCMFSA_2:85; :: thesis: verum

end;

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