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

proof

set D = { (l + (card I)) where l is Element of NAT : l in dom (ProgramPart J) } ;
let m, n be Nat; :: according to AFINSQ_1:def 13 :: thesis: ( not n in proj1 ((Directed I) +* (ProgramPart (Relocated (J,(card I))))) or n <= m or m in proj1 ((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 proj1 ((Directed I) +* (ProgramPart (Relocated (J,(card I)))))
ProgramPart (Relocated (J,(card I))) = Reloc ((ProgramPart J),(card I)) by COMPOS_1:116;
then ( dom (Directed I) = dom I & dom (ProgramPart (Relocated (J,(card I)))) = { (l + (card I)) where l is Element of NAT : l in dom (ProgramPart J) } ) by COMPOS_1:117, FUNCT_4:105;
then A3: 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 FUNCT_4:def 1;

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

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

then m in dom I by A2, AFINSQ_1:def 13;
hence m in proj1 ((Directed I) +* (ProgramPart (Relocated (J,(card I))))) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

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

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

now

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

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

then m in dom I by AFINSQ_1:70;
hence m in dom ((Directed I) +* (ProgramPart (Relocated (J,(card I))))) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

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

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

end;

end;

end;

hence m in proj1 ((Directed I) +* (ProgramPart (Relocated (J,(card I))))) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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