let x be set ; :: thesis: for i, m, n being Element of NAT holds
( not x in dom (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) 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 n,SCM+FSA )) or x = intloc i or x = IC SCM+FSA )
set iS = ((intloc i) .--> m) +* (Start-At n,SCM+FSA );
( dom ((intloc i) .--> m) = {(intloc i)} & dom (Start-At n,SCM+FSA ) = {(IC SCM+FSA )} ) by FUNCOP_1:19;
then A1: dom (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) = {(intloc i)} \/ {(IC SCM+FSA )} by FUNCT_4:def 1;
assume x in dom (((intloc i) .--> m) +* (Start-At n,SCM+FSA )) ; :: thesis: ( x = intloc i or x = IC SCM+FSA )
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