A1
:
[#]
K
=
[#]
V
by
SIMPLEX0:def 10
;
then
|.
K
.|
c=
[#]
K
;
then
[#]
(
BCS
(
n
,
K
)
)
=
[#]
V
by
A1
,
Th18
;
hence
BCS
(
n
,
K
) is
total
;
:: thesis:
verum