let a be Real; :: thesis: for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f holds
a * f = a * f1
let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace
for f being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f holds
a * f = a * f1
let Y be RealNormSpace; :: thesis: for f being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f holds
a * f = a * f1
let f be Point of (R_NormSpace_of_ContinuousFunctions (X,Y)); :: thesis: for f1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f holds
a * f = a * f1
let f1 be Point of (R_NormSpace_of_BoundedFunctions (X,Y)); :: thesis: ( f1 = f implies a * f = a * f1 )
assume A1: f1 = f ; :: thesis: a * f = a * f1
reconsider f2 = f as Point of (R_VectorSpace_of_ContinuousFunctions (X,Y)) ;
reconsider f3 = f2 as Point of (R_VectorSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;
A2: R_VectorSpace_of_ContinuousFunctions (X,Y) is Subspace of R_VectorSpace_of_BoundedFunctions (X,Y) by RSSPACE:11;
thus a * f = a * f2
.= a * f3 by A2, RLSUB_1:14
.= a * f1 by A1 ; :: thesis: verum