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