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)
X: ( n in NAT & k in NAT ) by ORDINAL1:def 13;
then n < len p by A3, SCMFSA_7:29;
then k < len p by A4, XXREAL_0:2;
hence k in dom (Load p) by A1, X; :: 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 consider m being Element of NAT such that
A5: ( m = x & m < len p ) by A1;
thus x in NAT by A5; :: 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