A1: dom (Load p) = { m where m is Element of NAT : m < len p } by Th1;

A2: now

let k, n be Nat; :: thesis: ( n in dom (Load p) & k < n implies k in dom (Load p) )
assume that
A3: n in dom (Load p) and
A4: k < n ; :: thesis: k in dom (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;

now

let x be set ; :: thesis: ( x in dom (Load p) implies 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;

then dom (Load p) c= NAT by TARSKI:def 3;
hence ( Load p is initial & Load p is NAT -defined ) by A2, RELAT_1:def 18, SCMNORM:def 1; :: thesis: verum