set P = I +* (Shift J,(card I));
I +* (Shift 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 13 :: thesis: ( not n in proj1 (I +* (Shift J,(card I))) or n <= m or m in proj1 (I +* (Shift J,(card I))) )
assume that
A1: n in dom (I +* (Shift J,(card I))) and
A2: m < n ; :: thesis: m in proj1 (I +* (Shift J,(card I)))
dom (Shift J,(card I)) = { (l + (card I)) where l is Element of NAT : l in dom J } by VALUED_1:def 12;
then A3: dom (I +* (Shift 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 (I +* (Shift J,(card I)))

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

then m in dom I by AFINSQ_1:70;
hence m in proj1 (I +* (Shift 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 13;
l1 < l by A2, A4, A6, XREAL_1:8;
then l1 in dom J by A5, AFINSQ_1:def 13;
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 (I +* (Shift J,(card I))) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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