take CAlgebra 1 ; :: thesis: ( CAlgebra 1 is strict & CAlgebra 1 is Abelian & CAlgebra 1 is add-associative & CAlgebra 1 is right_zeroed & CAlgebra 1 is right_complementable & CAlgebra 1 is commutative & CAlgebra 1 is associative & CAlgebra 1 is right_unital & CAlgebra 1 is right-distributive & CAlgebra 1 is vector-distributive & CAlgebra 1 is scalar-distributive & CAlgebra 1 is scalar-associative & CAlgebra 1 is vector-associative )
thus ( CAlgebra 1 is strict & CAlgebra 1 is Abelian & CAlgebra 1 is add-associative & CAlgebra 1 is right_zeroed & CAlgebra 1 is right_complementable & CAlgebra 1 is commutative & CAlgebra 1 is associative & CAlgebra 1 is right_unital & CAlgebra 1 is right-distributive & CAlgebra 1 is vector-distributive & CAlgebra 1 is scalar-distributive & CAlgebra 1 is scalar-associative & CAlgebra 1 is vector-associative ) ; :: thesis: verum