ProgramPart I is initial

proof

let m, n be Nat; :: according to SCMNORM:def 1 :: thesis: ( n in dom (ProgramPart I) & m < n implies m in dom (ProgramPart I) )
assume that
A1: n in dom (ProgramPart I) and
A2: m < n ; :: thesis: m in dom (ProgramPart I)
m in NAT by ORDINAL1:def 13;
then B: m is Instruction-Location of S by AMI_1:def 4;
ProgramPart I c= I by RELAT_1:88;
then dom (ProgramPart I) c= dom I by RELAT_1:25;
then m in dom I by A1, A2, Def1;
hence m in dom (ProgramPart I) by B, AMI_1:106; :: thesis: verum

end;

hence ProgramPart I is initial Function ; :: thesis: verum