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