take StructVectSp K ; :: thesis: ( StructVectSp K is Abelian & StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is VectSp-like & StructVectSp K is strict & not StructVectSp K is trivial )
thus ( StructVectSp K is Abelian & StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is VectSp-like & StructVectSp K is strict & not StructVectSp K is trivial ) ; :: thesis: verum