let I, J be Program of SCMPDS ; :: thesis: dom I misses dom (Shift J,(card I))
A1: dom (Shift J,(card I)) = { (l + (card I)) where l is Element of NAT : l in dom J } by VALUED_1:def 12;
assume dom I meets dom (Shift J,(card I)) ; :: thesis: contradiction
then consider x being set such that
A2: x in dom I and
A3: x in { (l + (card I)) where l is Element of NAT : l in dom J } by A1, XBOOLE_0:3;
consider l being Element of NAT such that
A4: x = l + (card I) and
l in dom J by A3;
l + (card I) < card I by A2, A4, Th1;
hence contradiction by NAT_1:11; :: thesis: verum