take StructVectSp K ; :: thesis: ( StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital & StructVectSp K is strict )
thus ( StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital & StructVectSp K is strict ) ; :: thesis: verum