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

now

let y be set ; :: thesis: ( y in rng p implies ex x being set st
( x in dom (Load p) & y = (Load p) . x ) )
assume y in rng p ; :: thesis: ex x being set st
( x in dom (Load p) & y = (Load p) . x )
then consider x being set such that
A2: x in dom p and
A3: y = p . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A2;
dom p = Seg (len p) by FINSEQ_1:def 3;
then dom p = { m where m is Element of NAT : ( 1 <= m & m <= len p ) } ;
then ex m being Element of NAT st
( x = m & 1 <= m & m <= len p ) by A2;
then A4: (x -' 1) + 1 = (x - 1) + 1 by XREAL_1:235
.= x ;
A5: x -' 1 in dom (Load p) by A1, A2;
then (Load p) . (x -' 1) = p /. ((x -' 1) + 1) by SCMFSA_7:def 1
.= y by A2, A3, A4, PARTFUN1:def 8 ;
hence ex x being set st
( x in dom (Load p) & y = (Load p) . x ) by A5; :: thesis: verum

end;

then A6: rng p c= rng (Load p) by FUNCT_1:19;

now

let y be set ; :: thesis: ( y in rng (Load p) implies ex x being set st
( x in dom p & y = p . x ) )
assume y in rng (Load p) ; :: thesis: ex x being set st
( x in dom p & y = p . x )
then consider x being set such that
A7: x in dom (Load p) and
A8: y = (Load p) . x by FUNCT_1:def 5;
consider m being Element of NAT such that
A9: x = m -' 1 and
m in dom p by A1, A7;
A10: (m -' 1) + 1 in dom p by A7, A9, SCMFSA_7:26;
then p . ((m -' 1) + 1) = p /. ((m -' 1) + 1) by PARTFUN1:def 8
.= y by A7, A8, A9, SCMFSA_7:def 1 ;
hence ex x being set st
( x in dom p & y = p . x ) by A10; :: thesis: verum

end;

then rng (Load p) c= rng p by FUNCT_1:19;
hence rng (Load p) = rng p by A6, XBOOLE_0:def 10; :: thesis: verum