let a be Real; :: thesis:
let X be non empty closed_interval Subset of REAL; :: thesis:
let Y be RealNormSpace; :: thesis:
let f, h be VECTOR of (R_VectorSpace_of_ContinuousFunctions (X,Y)); :: thesis:
A1: R_VectorSpace_of_ContinuousFunctions (X,Y) is Subspace of R_VectorSpace_of_BoundedFunctions (X,Y) by RSSPACE:11;
then reconsider f1 = f as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) by A1, RLSUB_1:10;
let f9, h9 be continuous PartFunc of REAL,Y; :: thesis:
assume A2: ( f9 = f & h9 = h & dom f9 = X & dom h9 = X ) ; :: thesis:
reconsider f90 = f1 as bounded Function of X,Y by RSSPACE4:def 5;
reconsider h90 = h1 as bounded Function of X,Y by RSSPACE4:def 5;

A3: now :: thesis:

assume A4: h = a * f ; :: thesis:
let x be Element of X; :: thesis:
A5: h1 = a * f1 by A1, A4, RLSUB_1:14;
thus h9 /. x = h90 . x by A2, PARTFUN1:def 6
.= a * (f90 /. x) by A5, RSSPACE4:9
.= a * (f9 /. x) by A2 ; :: thesis:

end;

now :: thesis:

assume A6: for x being Element of X holds h9 /. x = a * (f9 /. x) ; :: thesis:

now :: thesis:

let x be Element of X; :: thesis:
thus h90 . x = h9 /. x by A2, PARTFUN1:def 6
.= a * (f90 /. x) by A2, A6
.= a * (f90 . x) ; :: thesis:

end;

then h1 = a * f1 by RSSPACE4:9;
hence h = a * f by A1, RLSUB_1:14; :: thesis:

end;

hence ( h = a * f iff for x being Element of X holds h9 /. x = a * (f9 /. x) ) by A3; :: thesis: