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