now

let m, n be Nat; :: thesis: ( n in dom (IncAddr I,k) & m < n implies m in dom (IncAddr I,k) )
assume A1: n in dom (IncAddr I,k) ; :: thesis: ( m < n implies m in dom (IncAddr I,k) )
A2: dom (IncAddr I,k) = dom I by SCMFSA_4:def 6;
assume m < n ; :: thesis: m in dom (IncAddr I,k)
hence m in dom (IncAddr I,k) by A1, A2, SCMNORM:def 1; :: thesis: verum

end;

hence ( IncAddr I,k is initial & IncAddr I,k is NAT -defined ) by SCMNORM:def 1; :: thesis: verum