let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for I being Program of {INT,(INT *)} holds (Initialized I) +* (f .--> w) is 0 -started
let f be FinSeq-Location ; :: thesis: for I being Program of {INT,(INT *)} holds (Initialized I) +* (f .--> w) is 0 -started
let I be Program of {INT,(INT *)}; :: thesis: (Initialized I) +* (f .--> w) is 0 -started
set p = Initialized I;
set s = f .--> w;
A1: dom (Initialized I) misses dom (f .--> w) by Th46;
then A2: Initialized I c= (Initialized I) +* (f .--> w) by FUNCT_4:33;
A3: dom (Initialized I) = (dom I) \/ {(intloc 0),(IC SCM+FSA)} by Th41;
A4: dom (Initialized I) c= dom ((Initialized I) +* (f .--> w)) by A2, RELAT_1:25;
IC SCM+FSA in {(intloc 0),(IC SCM+FSA)} by TARSKI:def 2;
then A5: IC SCM+FSA in dom (Initialized I) by A3, XBOOLE_0:def 3;
then A6: not IC SCM+FSA in dom (f .--> w) by A1, XBOOLE_0:3;
thus IC SCM+FSA in dom ((Initialized I) +* (f .--> w)) by A4, A5; :: according to COMPOS_1:def 16 :: thesis: IC ((Initialized I) +* (f .--> w)) = 0
thus IC ((Initialized I) +* (f .--> w)) = IC (Initialized I) by A6, FUNCT_4:12
.= 0 by SCMFSA6A:46 ; :: thesis: verum