let I be Program of SCM+FSA; :: thesis: for i, m, n being Element of NAT holds dom I misses dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA)))
let i, m, n be Element of NAT ; :: thesis: dom I misses dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA)))
set iS = ((intloc i) .--> m) +* (Start-At (n,SCM+FSA));
assume (dom I) /\ (dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA)))) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being set such that
A1: x in (dom I) /\ (dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA)))) by XBOOLE_0:def 1;
A2: x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) by A1, XBOOLE_0:def 4;
A3: x in dom I by A1, XBOOLE_0:def 4;
dom I c= NAT by RELAT_1:def 18;
then reconsider x = x as Element of NAT by A3;

per cases ( x = intloc i or x = IC SCM+FSA ) by A2, Th1;

suppose x = intloc i ; :: thesis: contradiction

hence contradiction by SCMFSA_2:84; :: thesis: verum

end;

suppose x = IC SCM+FSA ; :: thesis: contradiction

hence contradiction by COMPOS_1:3; :: thesis: verum

end;

end;