let s be State of SCM+FSA; :: thesis: for iloc being Nat

for a being FinSeq-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a

let iloc be Nat; :: thesis: for a being FinSeq-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a

let a be FinSeq-Location ; :: thesis: s . a = (s +* (Start-At (iloc,SCM+FSA))) . a

a in the carrier of SCM+FSA ;

then a in dom s by PARTFUN1:def 2;

then A1: ( dom (Start-At (iloc,SCM+FSA)) = {(IC )} & a in (dom s) \/ (dom (Start-At (iloc,SCM+FSA))) ) by XBOOLE_0:def 3;

a <> IC by SCMFSA_2:57;

then not a in {(IC )} by TARSKI:def 1;

hence s . a = (s +* (Start-At (iloc,SCM+FSA))) . a by A1, FUNCT_4:def 1; :: thesis: verum

for a being FinSeq-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a

let iloc be Nat; :: thesis: for a being FinSeq-Location holds s . a = (s +* (Start-At (iloc,SCM+FSA))) . a

let a be FinSeq-Location ; :: thesis: s . a = (s +* (Start-At (iloc,SCM+FSA))) . a

a in the carrier of SCM+FSA ;

then a in dom s by PARTFUN1:def 2;

then A1: ( dom (Start-At (iloc,SCM+FSA)) = {(IC )} & a in (dom s) \/ (dom (Start-At (iloc,SCM+FSA))) ) by XBOOLE_0:def 3;

a <> IC by SCMFSA_2:57;

then not a in {(IC )} by TARSKI:def 1;

hence s . a = (s +* (Start-At (iloc,SCM+FSA))) . a by A1, FUNCT_4:def 1; :: thesis: verum