let s be State of SCM+FSA ; :: thesis:
assume A1: ( IC s = 0 & s . (intloc 0 ) = 1 ) ; :: thesis:
let a be Int-Location ; :: thesis:
let k be Integer; :: thesis:
assume that
A2: Load (aSeq a,k) c= s and
A3: a <> intloc 0 ; :: thesis:
A4: dom (Load (aSeq a,k)) = { (m -' 1) where m is Element of NAT : m in dom (aSeq a,k) } by Def1;

A5: now

let c be Element of NAT ; :: thesis:
assume A6: c in dom (aSeq a,k) ; :: thesis:
then c in Seg (len (aSeq a,k)) by FINSEQ_1:def 3;
then 1 <= c by FINSEQ_1:3;
then A7: c -' 1 = c - 1 by XREAL_1:235;
A8: c -' 1 in dom (Load (aSeq a,k)) by A4, A6;
then (Load (aSeq a,k)) . (c -' 1) = (aSeq a,k) /. ((c -' 1) + 1) by Def1
.= (aSeq a,k) . c by A6, A7, PARTFUN1:def 8 ;
hence (aSeq a,k) . c = s . ((0 + c) -' 1) by A2, A8, GRFUNC_1:8; :: thesis:

end;

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A9: i <= len (aSeq a,k) ; :: thesis:
then IC (Comput (ProgramPart s),s,i) = 0 + i by A1, A3, A5, Th36;
hence ( IC (Comput (ProgramPart s),s,i) = i & ( for b being Int-Location st b <> a holds
(Comput (ProgramPart s),s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s),s,i) . f = s . f ) ) by A1, A3, A5, A9, Th36; :: thesis:

end;

thus (Comput (ProgramPart s),s,(len (aSeq a,k))) . a = k by A1, A3, A5, Th36; :: thesis: