let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for I being Program of SCM+FSA holds (Initialized I) +* (f .--> w) starts_at 0
let f be FinSeq-Location ; :: thesis: for I being Program of SCM+FSA holds (Initialized I) +* (f .--> w) starts_at 0
let I be Program of SCM+FSA ; :: thesis: (Initialized I) +* (f .--> w) starts_at 0
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 AMI_1:def 44 :: thesis: IC ((Initialized I) +* (f .--> w)) = 0
thus IC ((Initialized I) +* (f .--> w)) = ((Initialized I) +* (f .--> w)) . (IC SCM+FSA ) by A4, A5, AMI_1:def 43
.= (Initialized I) . (IC SCM+FSA ) by A6, FUNCT_4:12
.= 0 by SCMFSA6A:46 ; :: thesis: verum