now

let m, n be Nat; :: thesis: ( n in dom (Initialized I) & m < n implies m in dom (Initialized I) )
I c= Initialized I by SCMFSA6A:26;
then A1: dom I c= dom (Initialized I) by GRFUNC_1:8;
X: n in NAT by ORDINAL1:def 13;
assume n in dom (Initialized I) ; :: thesis: ( m < n implies m in dom (Initialized I) )
then A2: n in dom I by X, Th20;
assume m < n ; :: thesis: m in dom (Initialized I)
then m in dom I by A2, AFINSQ_1:def 13;
hence m in dom (Initialized I) by A1; :: thesis: verum

end;

hence Initialized I is initial by AFINSQ_1:def 13; :: thesis: verum