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 (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
A2: ( x in dom (Load p) & y = (Load p) . x ) by FUNCT_1:def 5;
consider m being Element of NAT such that
A3: ( x = m -' 1 & m in dom p ) by A1, A2;
A4: (m -' 1) + 1 in dom p by A2, A3, SCMFSA_7:26;
then p . ((m -' 1) + 1) = p /. ((m -' 1) + 1) by PARTFUN1:def 8
.= y by A2, A3, SCMFSA_7:def 1 ;
hence ex x being set st
( x in dom p & y = p . x ) by A4; :: thesis: verum

end;

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

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
A6: ( x in dom p & y = p . x ) by FUNCT_1:def 5;
A7: dom p = Seg (len p) by FINSEQ_1:def 3;
reconsider x = x as Element of NAT by A6;
A8: insloc (x -' 1) in dom (Load p) by A1, A6;
dom p = { m where m is Element of NAT : ( 1 <= m & m <= len p ) } by A7, FINSEQ_1:def 1;
then consider m being Element of NAT such that
A9: ( x = m & 1 <= m & m <= len p ) by A6;
A10: (x -' 1) + 1 = (x - 1) + 1 by A9, XREAL_1:235
.= x ;
(Load p) . (insloc (x -' 1)) = p /. ((x -' 1) + 1) by A8, SCMFSA_7:def 1
.= y by A6, A10, PARTFUN1:def 8 ;
hence ex x being set st
( x in dom (Load p) & y = (Load p) . x ) by A8; :: thesis: verum

end;

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