let
A
,
B
be
Sequence
;
:: thesis:
rng
(
A
^
B
)
=
(
rng
A
)
\/
(
rng
B
)
(
rng
A
c=
rng
(
A
^
B
)
&
rng
B
c=
rng
(
A
^
B
)
)
by
Th7A
,
Th8A
;
then
A1
:
(
rng
A
)
\/
(
rng
B
)
c=
rng
(
A
^
B
)
by
XBOOLE_1:8
;
rng
(
A
^
B
)
c=
(
rng
A
)
\/
(
rng
B
)
by
Th2Lem
;
hence
rng
(
A
^
B
)
=
(
rng
A
)
\/
(
rng
B
)
by
A1
;
:: thesis:
verum