set
P
=
I
^
J
;
A1
: not
halt
S
in
rng
I
by
COMPOS_1:def 11
;
A2
: not
halt
S
in
rng
J
by
COMPOS_1:def 11
;
rng
(
I
^
J
)
=
(
rng
I
)
\/
(
rng
J
)
by
AFINSQ_1:26
;
then
not
halt
S
in
rng
(
I
^
J
)
by
A1
,
A2
,
XBOOLE_0:def 3
;
hence
I
^
J
is
halt-free
;
:: thesis:
verum