now

let v be VECTOR of (C_Algebra_of_BoundedFunctions X); :: thesis: 1r * v = v
reconsider v1 = v as VECTOR of (CAlgebra X) by TARSKI:def 3;
C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;
then 1r * v = 1r * v1 by Th4;
hence 1r * v = v by CFUNCDOM:12; :: thesis: verum

end;

hence ( C_Algebra_of_BoundedFunctions X is vector-distributive & C_Algebra_of_BoundedFunctions X is scalar-unital ) by CLVECT_1:def 5; :: thesis: verum