now :: thesis: for v being VECTOR of (C_Algebra_of_BoundedFunctions X) holds 1r * v = v

hence
( C_Algebra_of_BoundedFunctions X is vector-distributive & C_Algebra_of_BoundedFunctions X is scalar-unital )
; :: thesis: verumlet 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;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