A1: dom (Load p) = { m where m is Element of NAT : m < len p } by Th1;
thus Load p is initial :: thesis: ( Load p is NAT -defined & Load p is the Instructions of SCM+FSA -valued )

proof

let k, n be Nat; :: according to AFINSQ_1:def 13 :: thesis: ( not n in proj1 (Load p) or n <= k or k in proj1 (Load p) )
assume that
A3: n in dom (Load p) and
A4: k < n ; :: thesis: k in proj1 (Load p)
n in NAT by ORDINAL1:def 13;
then n < len p by A3, SCMFSA_7:29;
then ( k in NAT & k < len p ) by A4, ORDINAL1:def 13, XXREAL_0:2;
hence k in dom (Load p) by A1; :: thesis: verum

end;

thus Load p is NAT -defined :: thesis: Load p is the Instructions of SCM+FSA -valued

proof

let x be set ; :: according to TARSKI:def 3,RELAT_1:def 18 :: thesis: ( not x in proj1 (Load p) or x in NAT )
assume x in dom (Load p) ; :: thesis: x in NAT
then ex m being Element of NAT st
( m = x & m < len p ) by A1;
hence x in NAT ; :: thesis: verum

end;

rng (Load p) = rng p by Th2;
hence rng (Load p) c= the Instructions of SCM+FSA by FINSEQ_1:def 4; :: according to RELAT_1:def 19 :: thesis: verum