let t be FinSequence of INT ; :: thesis: for f being FinSeq-Location holds dom (Initialize ((intloc 0) .--> 1)) misses dom (f .--> t)
let f be FinSeq-Location ; :: thesis: dom (Initialize ((intloc 0) .--> 1)) misses dom (f .--> t)
set x = f .--> t;
set DI = dom (Initialize ((intloc 0) .--> 1));
assume (dom (Initialize ((intloc 0) .--> 1))) /\ (dom (f .--> t)) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider y being object such that
A2: y in (dom (Initialize ((intloc 0) .--> 1))) /\ (dom (f .--> t)) by XBOOLE_0:def 1;
A3: y in dom (Initialize ((intloc 0) .--> 1)) by A2, XBOOLE_0:def 4;
y in dom (f .--> t) by A2, XBOOLE_0:def 4;
then A4: y = f by TARSKI:def 1;
( y = intloc 0 or y = IC ) by A3, Th11, TARSKI:def 2;
hence contradiction by A4, SCMFSA_2:57, SCMFSA_2:58; :: thesis: verum