let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace
for a being Real
for x being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x = y holds
a * x = a * y
let T be NormedLinearTopSpace; :: thesis: for a being Real
for x being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x = y holds
a * x = a * y
let a be Real; :: thesis: for x being Point of (R_NormSpace_of_ContinuousFunctions (S,T))
for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x = y holds
a * x = a * y
let x be Point of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: for y being Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st x = y holds
a * x = a * y
let y be Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,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 S,T)) | [:REAL,(ContinuousFunctions (S,T)):]) . [a,x] by RSSPACE:def 9, Th5
.= the Mult of (RealVectSpace ( the carrier of S,T)) . [aa,x] by FUNCT_1:49
.= ( the Mult of (RealVectSpace ( the carrier of S,T)) | [:REAL,(BoundedFunctions ( the carrier of S,T)):]) . [aa,y] by A1, FUNCT_1:49
.= a * y by RSSPACE:def 9, RSSPACE4:6 ; :: thesis: verum