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