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 AMISTD_2:def 15;
assume m < n ; :: thesis: m in dom (IncAddr I,k)
hence m in dom (IncAddr I,k) by A1, A2, AFINSQ_1:def 13; :: thesis: verum

end;

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