let s be State of ; :: thesis: ( IC s = insloc 0 & s . (intloc 0 ) = 1 implies for a being Int-Location
for k being Integer st Load (aSeq a,k) c= s & a <> intloc 0 holds
( ( for i being Element of NAT st i <= len (aSeq a,k) holds
( IC (Computation s,i) = insloc i & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) ) & (Computation s,(len (aSeq a,k))) . a = k ) )
assume A1: ( IC s = insloc 0 & s . (intloc 0 ) = 1 ) ; :: thesis: for a being Int-Location
for k being Integer st Load (aSeq a,k) c= s & a <> intloc 0 holds
( ( for i being Element of NAT st i <= len (aSeq a,k) holds
( IC (Computation s,i) = insloc i & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) ) & (Computation s,(len (aSeq a,k))) . a = k )
let a be Int-Location ; :: thesis: for k being Integer st Load (aSeq a,k) c= s & a <> intloc 0 holds
( ( for i being Element of NAT st i <= len (aSeq a,k) holds
( IC (Computation s,i) = insloc i & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) ) & (Computation s,(len (aSeq a,k))) . a = k )
let k be Integer; :: thesis: ( Load (aSeq a,k) c= s & a <> intloc 0 implies ( ( for i being Element of NAT st i <= len (aSeq a,k) holds
( IC (Computation s,i) = insloc i & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) ) & (Computation s,(len (aSeq a,k))) . a = k ) )
assume that
A2: Load (aSeq a,k) c= s and
A3: a <> intloc 0 ; :: thesis: ( ( for i being Element of NAT st i <= len (aSeq a,k) holds
( IC (Computation s,i) = insloc i & ( for b being Int-Location st b <> a holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) ) & (Computation s,(len (aSeq a,k))) . a = k )
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: ( c in dom (aSeq a,k) implies (aSeq a,k) . c = s . (insloc ((0 + c) -' 1)) )
assume A6: c in dom (aSeq a,k) ; :: thesis: (aSeq a,k) . c = s . (insloc ((0 + c) -' 1))
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: insloc (c -' 1) in dom (Load (aSeq a,k)) by A4, A6;
then (Load (aSeq a,k)) . (insloc (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 . (insloc ((0 + c) -' 1)) by A2, A8, GRFUNC_1:8; :: thesis: verum

end;

hereby :: thesis: (Computation s,(len (aSeq a,k))) . a = k

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

end;

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