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