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 by SIMPLEX0:def 10; :: thesis: verum