let s be State of SCM+FSA; :: thesis: for l being Element of NAT holds dom (ProgramPart s) misses dom (Start-At (l,SCM+FSA))
let l be Element of NAT ; :: thesis: dom (ProgramPart s) misses dom (Start-At (l,SCM+FSA))

now

let x be set ; :: thesis: ( x in dom (ProgramPart s) implies not x in dom (Start-At (l,SCM+FSA)) )
assume x in dom (ProgramPart s) ; :: thesis: not x in dom (Start-At (l,SCM+FSA))
then x in NAT by COMPOS_1:34;
then x is Element of NAT ;
then x <> IC SCM+FSA by COMPOS_1:3;
then not x in {(IC SCM+FSA)} by TARSKI:def 1;
hence not x in dom (Start-At (l,SCM+FSA)) by FUNCOP_1:19; :: thesis: verum

end;

hence dom (ProgramPart s) misses dom (Start-At (l,SCM+FSA)) by XBOOLE_0:3; :: thesis: verum