for v being Element of (CAlgebra X) holds 1r * v = v by CFUNCDOM:12;
hence CAlgebra X is scalar-unital by CLVECT_1:def 5; :: thesis: verum