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

now

let x be set ; :: thesis: not x in dom (DataPart (I +* (Start-At (insloc 0 ))))
assume x in dom (DataPart (I +* (Start-At (insloc 0 )))) ; :: thesis: contradiction
then A1: x in (dom (I +* (Start-At (insloc 0 )))) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then A2: ( x in dom (I +* (Start-At (insloc 0 ))) & x in Int-Locations \/ FinSeq-Locations ) by XBOOLE_0:def 4;
then x in (dom I) \/ (dom (Start-At (insloc 0 ))) 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 Instruction-Location of SCM+FSA by A4, AMI_1:def 4;
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 (insloc 0 )))) = {} by XBOOLE_0:def 1;
hence DataPart (I +* (Start-At (insloc 0 ))) = {} by RELAT_1:64; :: thesis: verum