let p be FinSequence of the Instructions of SCM+FSA ; :: thesis: dom (Load p) = { m where m is Element of NAT : m < len p }
A1: dom (Load p) = { (m -' 1) where m is Element of NAT : m in dom p } by SCMFSA_7:def 1;

now

let x be set ; :: thesis: ( x in dom (Load p) implies x in { m where m is Element of NAT : m < len p } )
assume A2: x in dom (Load p) ; :: thesis: x in { m where m is Element of NAT : m < len p }
then consider k being Element of NAT such that
A3: x = k -' 1 and
k in dom p by A1;
k -' 1 < len p by A2, A3, SCMFSA_7:29;
hence x in { m where m is Element of NAT : m < len p } by A3; :: thesis: verum

end;

then A4: dom (Load p) c= { m where m is Element of NAT : m < len p } by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in { m where m is Element of NAT : m < len p } implies x in dom (Load p) )
assume x in { m where m is Element of NAT : m < len p } ; :: thesis: x in dom (Load p)
then ex k being Element of NAT st
( x = k & k < len p ) ;
hence x in dom (Load p) by SCMFSA_7:29; :: thesis: verum

end;

then { m where m is Element of NAT : m < len p } c= dom (Load p) by TARSKI:def 3;
hence dom (Load p) = { m where m is Element of NAT : m < len p } by A4, XBOOLE_0:def 10; :: thesis: verum