let x be set ; 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; ( 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)))
; ( 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; verum