A1
:
rng
(
p
^'
q
)
c=
(
rng
p
)
\/
(
rng
q
)
by
Th17
;
A2
:
rng
q
c=
D
by
FINSEQ_1:def 4
;
rng
p
c=
D
by
FINSEQ_1:def 4
;
then
(
rng
p
)
\/
(
rng
q
)
c=
D
by
A2
,
XBOOLE_1:8
;
then
rng
(
p
^'
q
)
c=
D
by
A1
;
hence
p
^'
q
is
FinSequence
of
D
by
FINSEQ_1:def 4
;
:: thesis:
verum