for v being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds 1r * v = v
proof
let v be Point of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: 1r * v = v
reconsider v1 = v as Element of CContinuousFunctions X ;
A1: 1r * v = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CContinuousFunctions X):]) . [1r,v1] by CC0SP1:def 3
.= the Mult of (CAlgebra the carrier of 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_ContinuousFunctions X is vector-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & C_Normed_Algebra_of_ContinuousFunctions X is scalar-unital ) ; :: thesis: verum