let I be Program of SCM+FSA; :: thesis: DataPart (I +* (Start-At (0,SCM+FSA))) = {}
set SAt = Start-At (0,SCM+FSA);
set IAt = I +* (Start-At (0,SCM+FSA));

now

let x be set ; :: thesis: not x in dom (DataPart (I +* (Start-At (0,SCM+FSA))))
assume x in dom (DataPart (I +* (Start-At (0,SCM+FSA)))) ; :: thesis: contradiction
then A1: x in (dom (I +* (Start-At (0,SCM+FSA)))) /\ (Int-Locations \/ FinSeq-Locations) by RELAT_1:90, SCMFSA_2:127;
then A2: x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 4;
x in dom (I +* (Start-At (0,SCM+FSA))) 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 SCM+FSA)} by FUNCOP_1:19;
then A3: ( x in dom I or x in {(IC SCM+FSA)} ) by XBOOLE_0:def 3;

per cases ( x in dom I or x = IC SCM+FSA ) 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 SCM+FSA ; :: thesis: contradiction

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

end;

end;

end;

then dom (DataPart (I +* (Start-At (0,SCM+FSA)))) = {} by XBOOLE_0:def 1;
hence DataPart (I +* (Start-At (0,SCM+FSA))) = {} ; :: thesis: verum