let x be set ; :: thesis: for i, m, n being Element of NAT holds
( not x in dom (((intloc i) .--> m) +* (Start-At (insloc n))) or x = intloc i or x = IC SCM+FSA )
let i, m, n be Element of NAT ; :: thesis: ( not x in dom (((intloc i) .--> m) +* (Start-At (insloc n))) or x = intloc i or x = IC SCM+FSA )
set iS = ((intloc i) .--> m) +* (Start-At (insloc n));
assume A1: x in dom (((intloc i) .--> m) +* (Start-At (insloc n))) ; :: thesis: ( x = intloc i or x = IC SCM+FSA )
A2: dom ((intloc i) .--> m) = {(intloc i)} by FUNCOP_1:19;
dom (Start-At (insloc n)) = {(IC SCM+FSA )} by FUNCOP_1:19;
then dom (((intloc i) .--> m) +* (Start-At (insloc n))) = {(intloc i)} \/ {(IC SCM+FSA )} by A2, FUNCT_4:def 1;
then ( x in {(intloc i)} or x in {(IC SCM+FSA )} ) by A1, XBOOLE_0:def 3;
hence ( x = intloc i or x = IC SCM+FSA ) by TARSKI:def 1; :: thesis: verum