set W = ContinuousFunctions (X,Y);
thus for v, u being VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)) st v in ContinuousFunctions (X,Y) & u in ContinuousFunctions (X,Y) holds
v + u in ContinuousFunctions (X,Y) :: according to RLSUB_1:def 1 :: thesis: for b₁ being object
for b₂ being Element of the carrier of (R_VectorSpace_of_BoundedFunctions (X,Y)) holds
( not b₂ in ContinuousFunctions (X,Y) or b₁ * b₂ in ContinuousFunctions (X,Y) )

proof

let v, u be VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)); :: thesis: ( v in ContinuousFunctions (X,Y) & u in ContinuousFunctions (X,Y) implies v + u in ContinuousFunctions (X,Y) )
assume that
A1: v in ContinuousFunctions (X,Y) and
A2: u in ContinuousFunctions (X,Y) ; :: thesis: v + u in ContinuousFunctions (X,Y)
reconsider f = v + u, v0 = v, u0 = u as bounded Function of X,Y by RSSPACE4:def 5;
consider v1 being continuous PartFunc of REAL,Y such that
A3: ( v1 = v & dom v1 = X ) by A1, Def2;
consider u1 being continuous PartFunc of REAL,Y such that
A4: ( u1 = u & dom u1 = X ) by A2, Def2;
A5: dom f = (dom v1) /\ (dom u1) by A3, A4, FUNCT_2:def 1;

A6: now :: thesis: for x0 being Element of REAL st x0 in dom f holds
f /. x0 = (v1 /. x0) + (u1 /. x0)

let x0 be Element of REAL ; :: thesis: ( x0 in dom f implies f /. x0 = (v1 /. x0) + (u1 /. x0) )
assume A7: x0 in dom f ; :: thesis: f /. x0 = (v1 /. x0) + (u1 /. x0)
then reconsider x = x0 as Element of X ;
thus f /. x0 = f . x by A7, PARTFUN1:def 6
.= (v0 /. x) + (u0 /. x) by RSSPACE4:8
.= (v1 /. x0) + (u1 /. x0) by A3, A4 ; :: thesis: verum

end;

dom f = X by FUNCT_2:def 1;
then ( dom f c= REAL & rng f c= the carrier of Y ) ;
then f in PFuncs (REAL, the carrier of Y) by PARTFUN1:def 3;
then f is PartFunc of REAL,Y by PARTFUN1:46;
then A8: f = v1 + u1 by A5, A6, VFUNCT_1:def 1;
then dom (v1 + u1) = X by FUNCT_2:def 1;
hence v + u in ContinuousFunctions (X,Y) by Def2, A8; :: thesis: verum

end;

let a be Real; :: thesis: for b₁ being Element of the carrier of (R_VectorSpace_of_BoundedFunctions (X,Y)) holds
( not b₁ in ContinuousFunctions (X,Y) or a * b₁ in ContinuousFunctions (X,Y) )
let v be VECTOR of (R_VectorSpace_of_BoundedFunctions (X,Y)); :: thesis: ( not v in ContinuousFunctions (X,Y) or a * v in ContinuousFunctions (X,Y) )
assume A9: v in ContinuousFunctions (X,Y) ; :: thesis: a * v in ContinuousFunctions (X,Y)
reconsider f = a * v, v0 = v as bounded Function of X,Y by RSSPACE4:def 5;
consider v1 being continuous PartFunc of REAL,Y such that
A10: ( v1 = v & dom v1 = X ) by A9, Def2;
A11: dom f = dom v1 by A10, FUNCT_2:def 1;

A12: now :: thesis: for x0 being Element of REAL st x0 in dom f holds
f /. x0 = a * (v1 /. x0)

let x0 be Element of REAL ; :: thesis: ( x0 in dom f implies f /. x0 = a * (v1 /. x0) )
assume A13: x0 in dom f ; :: thesis: f /. x0 = a * (v1 /. x0)
then reconsider x = x0 as Element of X ;
thus f /. x0 = f . x by A13, PARTFUN1:def 6
.= a * (v0 /. x) by RSSPACE4:9
.= a * (v1 /. x0) by A10 ; :: thesis: verum

end;

dom f = X by FUNCT_2:def 1;
then ( dom f c= REAL & rng f c= the carrier of Y ) ;
then f in PFuncs (REAL, the carrier of Y) by PARTFUN1:def 3;
then f is PartFunc of REAL,Y by PARTFUN1:46;
then A14: f = a (#) v1 by A11, A12, VFUNCT_1:def 4;
then dom (a (#) v1) = X by FUNCT_2:def 1;
hence a * v in ContinuousFunctions (X,Y) by Def2, A14; :: thesis: verum