let X be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace
for a being Real
for x being Point of (R_Normed_Space_of_C_0_Functions (X,T))
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) st x = y holds
a * x = a * y
let T be NormedLinearTopSpace; :: thesis: for a being Real
for x being Point of (R_Normed_Space_of_C_0_Functions (X,T))
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) st x = y holds
a * x = a * y
let a be Real; :: thesis: for x being Point of (R_Normed_Space_of_C_0_Functions (X,T))
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) st x = y holds
a * x = a * y
let x be Point of (R_Normed_Space_of_C_0_Functions (X,T)); :: thesis: for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)) st x = y holds
a * x = a * y
let y be Point of (R_NormSpace_of_BoundedFunctions ( the carrier of X,T)); :: thesis: ( x = y implies a * x = a * y )
assume A1: x = y ; :: thesis: a * x = a * y
reconsider aa = a as Element of REAL by XREAL_0:def 1;
thus a * x = ( the Mult of (RealVectSpace ( the carrier of X,T)) | [:REAL,(C_0_Functions (X,T)):]) . [a,x] by RSSPACE:def 9
.= the Mult of (RealVectSpace ( the carrier of X,T)) . [aa,x] by FUNCT_1:49
.= ( the Mult of (RealVectSpace ( the carrier of X,T)) | [:REAL,(BoundedFunctions ( the carrier of X,T)):]) . [aa,y] by A1, FUNCT_1:49
.= a * y by RSSPACE:def 9, RSSPACE4:6 ; :: thesis: verum