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 f be FinSeq-Location ; :: thesis: (IExec I,s) . f = (Result (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 (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 (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 (s +* (Initialized I))) . b by A1, FUNCT_4:12, SCMFSA_2:84; :: thesis: verum

end;

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