let s be State of SCM+FSA ; :: thesis: for iloc being Element of NAT
for a being FinSeq-Location holds s . a = (s +* (Start-At iloc,SCM+FSA )) . a
let iloc be Element of 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 4;
then A1: ( dom (Start-At iloc,SCM+FSA ) = {(IC SCM+FSA )} & a in (dom s) \/ (dom (Start-At iloc,SCM+FSA )) ) by FUNCOP_1:19, XBOOLE_0:def 3;
a <> IC SCM+FSA by SCMFSA_2:82;
then not a in {(IC SCM+FSA )} by TARSKI:def 1;
hence s . a = (s +* (Start-At iloc,SCM+FSA )) . a by A1, FUNCT_4:def 1; :: thesis: verum