set IJ = I ';' J;

now

set D = { (n + (card I)) where n is Element of NAT : n in dom J } ;
dom (Shift (J,(card I))) = { (n + (card I)) where n is Element of NAT : n in dom J } by VALUED_1:def 12;
then A1: dom (I ';' J) = (dom I) \/ { (n + (card I)) where n is Element of NAT : n in dom J } by FUNCT_4:def 1;
let x be Element of NAT ; :: thesis: ( x in dom (I ';' J) implies (I ';' J) . b₁ <> halt SCMPDS )
assume A2: x in dom (I ';' J) ; :: thesis: (I ';' J) . b₁ <> halt SCMPDS

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

suppose A3: x in dom I ; :: thesis: (I ';' J) . b₁ <> halt SCMPDS

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

end;

suppose x in { (n + (card I)) where n is Element of NAT : n in dom J } ; :: thesis: (I ';' J) . b₁ <> halt SCMPDS

then consider n being Element of 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 4;
hence (I ';' J) . x <> halt SCMPDS by A5, Def3; :: thesis: verum

end;

end;

end;

hence I ';' J is halt-free by Def3; :: thesis: verum