let X be non empty compact TopSpace; :: thesis: for a being Real
for x being Point of
for y being Point of st x = y holds
a * x = a * y
let a be Real; :: thesis: for x being Point of
for y being Point of st x = y holds
a * x = a * y
let x be Point of ; :: thesis: for y being Point of st x = y holds
a * x = a * y
let y be Point of ; :: thesis: ( x = y implies a * x = a * y )
assume AS: x = y ; :: thesis: a * x = a * y
thus a * x = (the Mult of (RAlgebra the carrier of X) | [:REAL ,(ContinuousFunctions X):]) . [a,x] by C0SP1:def 11
.= the Mult of (RAlgebra the carrier of X) . [a,x] by FUNCT_1:72
.= (the Mult of (RAlgebra the carrier of X) | [:REAL ,(BoundedFunctions the carrier of X):]) . [a,y] by FUNCT_1:72, AS
.= a * y by C0SP1:def 11 ; :: thesis: verum