set IJ = I ';' J;
set D = { (n + (card I)) where n is Nat : n in dom J } ;
dom (Shift (J,(card I))) = { (n + (card I)) where n is Nat : n in dom J } by VALUED_1:def 12;
then A1: dom (I ';' J) = (dom I) \/ { (n + (card I)) where n is Nat : n in dom J } by FUNCT_4:def 1;
let x be Nat; :: according to COMPOS_1:def 27 :: thesis: ( not x in proj1 (I ';' J) or not (I ';' J) . x = halt SCMPDS )
assume A2: x in dom (I ';' J) ; :: thesis: not (I ';' J) . x = halt SCMPDS

per cases ( x in dom I or x in { (n + (card I)) where n is Nat : n in dom J } ) by A2, A1, XBOOLE_0:def 3;

suppose A3: x in dom I ; :: thesis: not (I ';' J) . x = halt SCMPDS

then I . x = (I ';' J) . x by AFINSQ_1:def 3;
hence (I ';' J) . x <> halt SCMPDS by A3, COMPOS_1:def 27; :: thesis: verum

end;

suppose x in { (n + (card I)) where n is Nat : n in dom J } ; :: thesis: not (I ';' J) . x = halt SCMPDS

then consider n being Nat such that
A4: x = n + (card I) and
A5: n in dom J ;
J . n = (I ';' J) . x by A4, A5, AFINSQ_1:def 3;
hence (I ';' J) . x <> halt SCMPDS by A5, COMPOS_1:def 27; :: thesis: verum

end;

end;