let t be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for I being Program of SCM+FSA holds dom (Initialized I) misses dom (f .--> t)
let f be FinSeq-Location ; :: thesis: for I being Program of SCM+FSA holds dom (Initialized I) misses dom (f .--> t)
let I be Program of SCM+FSA ; :: thesis: dom (Initialized I) misses dom (f .--> t)
set x = f .--> t;
A1: dom (f .--> t) = {f} by FUNCOP_1:19;
set DB = dom I;
set DI = dom (Initialized I);
A2: dom (Initialized I) = (dom I) \/ {(intloc 0 ),(IC SCM+FSA )} by Th41;
assume (dom (Initialized I)) /\ (dom (f .--> t)) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider y being set such that
A3: y in (dom (Initialized I)) /\ (dom (f .--> t)) by XBOOLE_0:def 1;
A4: ( y in dom (Initialized I) & y in dom (f .--> t) ) by A3, XBOOLE_0:def 4;
then A5: y = f by A1, TARSKI:def 1;
A6: dom I c= NAT by RELAT_1:def 18;

now

assume y in dom I ; :: thesis: contradiction
then reconsider y = y as Instruction-Location of SCM+FSA by A6, AMI_1:def 4;
y = y ;
hence contradiction by A5, SCMFSA_2:85; :: thesis: verum

end;

then y in {(intloc 0 ),(IC SCM+FSA )} by A2, A4, XBOOLE_0:def 3;
then ( y = intloc 0 or y = IC SCM+FSA ) by TARSKI:def 2;
hence contradiction by A5, SCMFSA_2:82, SCMFSA_2:83; :: thesis: verum