set I = (inspos 0 ) .--> i;
A1: dom ((inspos 0 ) .--> i) = {(inspos 0 )} by FUNCOP_1:19;
reconsider I = (inspos 0 ) .--> i as finite Function ;
reconsider I = I as FinPartState of SCMPDS ;
( I is initial & I is NAT -defined )

proof

thus I is initial :: thesis: I is NAT -defined

proof

let m, n be Nat; :: according to SCMNORM:def 1 :: thesis: ( not n in dom I or n <= m or m in dom I )
assume that
A2: n in dom I and
A3: m < n ; :: thesis: m in dom I
thus m in dom I by A1, A2, A3, TARSKI:def 1; :: thesis: verum

end;

thus dom I c= NAT by A1, ZFMISC_1:37; :: according to RELAT_1:def 18 :: thesis: verum

end;

hence (inspos 0 ) .--> i is Program of SCMPDS ; :: thesis: verum