let X be non empty set ; :: thesis: C_Normed_Algebra_of_BoundedFunctions X is ComplexLinearSpace
for v being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds 1r * v = v
proof
let v be Point of (C_Normed_Algebra_of_BoundedFunctions X); :: thesis: 1r * v = v
reconsider v1 = v as Element of ComplexBoundedFunctions X ;
A1: 1r * v = ( the Mult of (CAlgebra X) | [:COMPLEX,(ComplexBoundedFunctions X):]) . [1r,v1] by Def3
.= the Mult of (CAlgebra X) . (1r,v1) by FUNCT_1:49
.= v1 by CFUNCDOM:12 ;
thus 1r * v = v by A1; :: thesis: verum
end;
hence C_Normed_Algebra_of_BoundedFunctions X is ComplexLinearSpace by Th15, CLVECT_1:def 5; :: thesis: verum