now :: thesis: for v being VECTOR of (C_Algebra_of_BoundedFunctions X) holds 1r * v = v
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 Th3;
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 ) ; :: thesis: verum