set P = (Directed I) +* [(ProgramPart (Relocated J,(card I)))];
(Directed I) +* [(ProgramPart (Relocated J,(card I)))] is initial

proof

let m, n be Nat; :: according to SCMNORM:def 1 :: thesis: ( not n in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))]) or n <= m or m in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))]) )
assume that
A1: n in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))]) and
A2: m < n ; :: thesis: m in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))])
set D = { (l + (card I)) where l is Element of NAT : l in dom (ProgramPart J) } ;
A3: dom (Directed I) = dom I by FUNCT_4:105;
dom (ProgramPart (Relocated J,(card I))) = { (l + (card I)) where l is Element of NAT : l in dom (ProgramPart J) } by SCMFSA_5:3;
then A4: dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))]) = (dom I) \/ { (l + (card I)) where l is Element of NAT : l in dom (ProgramPart J) } by A3, FUNCT_4:def 1;

per cases ( insloc n in dom I or insloc n in { (l + (card I)) where l is Element of NAT : l in dom (ProgramPart J) } ) by A1, A4, XBOOLE_0:def 3;

suppose insloc n in dom I ; :: thesis: m in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))])

then insloc m in dom I by A2, SCMNORM:def 1;
hence m in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))]) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose insloc n in { (l + (card I)) where l is Element of NAT : l in dom (ProgramPart J) } ; :: thesis: m in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))])

then consider l being Element of NAT such that
A5: insloc n = l + (card I) and
A6: l in dom (ProgramPart J) ;

now

per cases ( m < card I or m >= card I ) ;

case m < card I ; :: thesis: insloc m in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))])

then insloc m in dom I by Th15;
hence insloc m in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))]) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

case m >= card I ; :: thesis: insloc m in { (l + (card I)) where l is Element of NAT : l in dom (ProgramPart J) }

then consider l1 being Nat such that
A7: m = (card I) + l1 by NAT_1:10;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def 13;
l1 < l by A2, A5, A7, XREAL_1:8;
then l1 in dom (ProgramPart J) by A6, SCMNORM:def 1;
hence insloc m in { (l + (card I)) where l is Element of NAT : l in dom (ProgramPart J) } by A7; :: thesis: verum

end;

end;

end;

hence m in dom ((Directed I) +* [(ProgramPart (Relocated J,(card I)))]) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence (Directed I) +* (ProgramPart (Relocated J,(card I))) is Program of SCM+FSA ; :: thesis: verum