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

proof

let m, n be Nat; :: according to SCMNORM:def 1 :: thesis: ( not n in proj1 I or n <= m or m in proj1 I )
assume ( n in dom I & m < n ) ; :: thesis: m in proj1 I
hence m in proj1 I by A1, TARSKI:def 1; :: thesis: verum

end;

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