let S, T be RealNormSpace; ContinuousFunctions (S,T) is linearly-closed
set W = ContinuousFunctions (S,T);
A1:
for v, u being VECTOR of (RealVectSpace ( the carrier of S,T)) st v in ContinuousFunctions (S,T) & u in ContinuousFunctions (S,T) holds
v + u in ContinuousFunctions (S,T)
proof
let v,
u be
VECTOR of
(RealVectSpace ( the carrier of S,T));
( v in ContinuousFunctions (S,T) & u in ContinuousFunctions (S,T) implies v + u in ContinuousFunctions (S,T) )
assume that A2:
v in ContinuousFunctions (
S,
T)
and A3:
u in ContinuousFunctions (
S,
T)
;
v + u in ContinuousFunctions (S,T)
consider f being
Function of the
carrier of
S, the
carrier of
T such that A4:
(
v = f &
f is_continuous_on the
carrier of
S )
by A2;
consider g being
Function of the
carrier of
S, the
carrier of
T such that A5:
(
u = g &
g is_continuous_on the
carrier of
S )
by A3;
reconsider u1 =
u as
Element of
Funcs ( the
carrier of
S, the
carrier of
T) ;
reconsider v1 =
v as
Element of
Funcs ( the
carrier of
S, the
carrier of
T) ;
reconsider h =
f + g as
Element of
Funcs ( the
carrier of
S, the
carrier of
T)
by FUNCT_2:8;
A6:
dom (f + g) =
(dom f) /\ (dom g)
by VFUNCT_1:def 1
.=
the
carrier of
S /\ (dom g)
by FUNCT_2:def 1
.=
the
carrier of
S /\ the
carrier of
S
by FUNCT_2:def 1
.=
the
carrier of
S
;
for
x being
Element of the
carrier of
S holds
h . x = (v1 . x) + (u1 . x)
then A7:
h = v + u
by LOPBAN_1:1;
f + g is_continuous_on the
carrier of
S
by A4, A5, NFCONT_1:25;
hence
v + u in ContinuousFunctions (
S,
T)
by A7;
verum
end;
for a being Real
for v being VECTOR of (RealVectSpace ( the carrier of S,T)) st v in ContinuousFunctions (S,T) holds
a * v in ContinuousFunctions (S,T)
proof
let a be
Real;
for v being VECTOR of (RealVectSpace ( the carrier of S,T)) st v in ContinuousFunctions (S,T) holds
a * v in ContinuousFunctions (S,T)let v be
VECTOR of
(RealVectSpace ( the carrier of S,T));
( v in ContinuousFunctions (S,T) implies a * v in ContinuousFunctions (S,T) )
assume
v in ContinuousFunctions (
S,
T)
;
a * v in ContinuousFunctions (S,T)
then consider f being
Function of the
carrier of
S, the
carrier of
T such that A9:
(
v = f &
f is_continuous_on the
carrier of
S )
;
reconsider v1 =
v as
Element of
Funcs ( the
carrier of
S, the
carrier of
T) ;
reconsider h =
a (#) f as
Element of
Funcs ( the
carrier of
S, the
carrier of
T)
by FUNCT_2:8;
A10:
dom (a (#) f) = the
carrier of
S
by FUNCT_2:def 1;
for
x being
Element of the
carrier of
S holds
h . x = a * (v1 . x)
then A11:
h = a * v
by LOPBAN_1:2;
a (#) f is_continuous_on the
carrier of
S
by A9, NFCONT_1:27;
hence
a * v in ContinuousFunctions (
S,
T)
by A11;
verum
end;
hence
ContinuousFunctions (S,T) is linearly-closed
by A1; verum