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

for v being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds 1r * v = v

proof

hence
C_Normed_Algebra_of_BoundedFunctions X is ComplexLinearSpace
by Th15, CLVECT_1:def 5; :: thesis: verum
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;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