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

proof

set D = { (l + (card I)) where l is Element of NAT : l in dom J } ;
let m, n be Nat; :: according to AFINSQ_1:def 12 :: thesis: ( not n in proj1 ((Directed I) +* (Reloc (J,(card I)))) or n <= m or m in proj1 ((Directed I) +* (Reloc (J,(card I)))) )
assume that
A1: n in dom ((Directed I) +* (Reloc (J,(card I)))) and
A2: m < n ; :: thesis: m in proj1 ((Directed I) +* (Reloc (J,(card I))))
( dom (Directed I) = dom I & dom (Reloc (J,(card I))) = { (l + (card I)) where l is Element of NAT : l in dom J } ) by COMPOS_1:33, FUNCT_4:99;
then A3: dom ((Directed I) +* (Reloc (J,(card I)))) = (dom I) \/ { (l + (card I)) where l is Element of NAT : l in dom 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 J } ) by A1, A3, XBOOLE_0:def 3;

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

then m in dom I by A2, AFINSQ_1:def 12;
hence m in proj1 ((Directed I) +* (Reloc (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 J } ; :: thesis: m in proj1 ((Directed I) +* (Reloc (J,(card I))))

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

now

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

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

then m in dom I by AFINSQ_1:66;
hence m in dom ((Directed I) +* (Reloc (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 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 12;
l1 < l by A2, A4, A6, XREAL_1:6;
then l1 in dom J by A5, AFINSQ_1:def 12;
hence m in { (l + (card I)) where l is Element of NAT : l in dom J } by A6; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

hence (Directed I) +* (Reloc (J,(card I))) is Program of ; :: thesis: verum