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 < len p )
let k be Element of NAT ; :: thesis: ( k in dom (Load p) iff k < len p )
A1: dom p = Seg (len p) by FINSEQ_1:def 3;

hereby :: thesis: ( k < len p implies k in dom (Load p) )

assume k in dom (Load p) ; :: thesis: k < len p
then k + 1 in dom p by Th26;
then k + 1 <= len p by A1, FINSEQ_1:3;
hence k < len p by NAT_1:13; :: thesis: verum

end;

assume k < len p ; :: thesis: k in dom (Load p)
then ( 1 <= k + 1 & k + 1 <= len p ) by NAT_1:11, NAT_1:13;
then k + 1 in Seg (len p) ;
hence k in dom (Load p) by A1, Th26; :: thesis: verum