let p be FinSequence of the Instructions of SCM+FSA ; :: thesis: for k being Element of NAT holds
( k in dom (Load p) iff k + 1 in dom p )
let k be Element of NAT ; :: thesis: ( k in dom (Load p) iff k + 1 in dom p )
A1: dom (Load p) = { (m -' 1) where m is Element of NAT : m in dom p } by Def1;

hereby :: thesis: ( k + 1 in dom p implies k in dom (Load p) )

assume k in dom (Load p) ; :: thesis: k + 1 in dom p
then consider m being Element of NAT such that
A2: m -' 1 = k and
A3: m in dom p by A1;
dom p = Seg (len p) by FINSEQ_1:def 3;
then 1 <= m by A3, FINSEQ_1:3;
then k + 1 = (m - 1) + 1 by A2, XREAL_1:235
.= m ;
hence k + 1 in dom p by A3; :: thesis: verum

end;

assume k + 1 in dom p ; :: thesis: k in dom (Load p)
then (k + 1) -' 1 in dom (Load p) by A1;
hence k in dom (Load p) by NAT_D:34; :: thesis: verum