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;
A1: dom (f .--> t) = {f} by FUNCOP_1:13;
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 set such that
A3: y in (dom (Initialize ((intloc 0) .--> 1))) /\ (dom (f .--> t)) by XBOOLE_0:def 1;
A4: y in dom (Initialize ((intloc 0) .--> 1)) by A3, XBOOLE_0:def 4;
y in dom (f .--> t) by A3, XBOOLE_0:def 4;
then A5: y = f by A1, TARSKI:def 1;
y in {(intloc 0),(IC )} by A4, SCMFSA6A:42;
then ( y = intloc 0 or y = IC ) by TARSKI:def 2;
hence contradiction by A5, SCMFSA_2:57, SCMFSA_2:58; :: thesis: verum