let I be Program of SCM+FSA; :: thesis: DataPart (Initialize I) = {}
set IAt = Initialize I;

now

let x be set ; :: thesis: not x in dom (DataPart (Initialize I))
assume x in dom (DataPart (Initialize I)) ; :: thesis: contradiction
then A1: x in (dom (Initialize I)) /\ (Data-Locations SCM+FSA) by RELAT_1:90;
then A2: x in Data-Locations SCM+FSA by XBOOLE_0:def 4;
x in dom (Initialize I) by A1, XBOOLE_0:def 4;
then x in (dom I) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1;
then x in (dom I) \/ {(IC )} by FUNCOP_1:19;
then A3: ( x in dom I or x in {(IC )} ) by XBOOLE_0:def 3;

per cases ( x in dom I or x = IC ) by A3, TARSKI:def 1;

suppose A4: x in dom I ; :: thesis: contradiction

dom I c= NAT by RELAT_1:def 18;
then reconsider x = x as Element of NAT by A4;
x in dom I by A4;
hence contradiction by A2, SCMFSA6A:37; :: thesis: verum

end;

suppose x = IC ; :: thesis: contradiction

hence contradiction by A1, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

then dom (DataPart (Initialize I)) = {} by XBOOLE_0:def 1;
hence DataPart (Initialize I) = {} ; :: thesis: verum