let X be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds
( ||.f.|| | X is continuous & (- f) | X is continuous )
let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds
( ||.f.|| | X is continuous & (- f) | X is continuous )
let f be PartFunc of REAL, the carrier of S; :: thesis: ( X c= dom f & f | X is continuous implies ( ||.f.|| | X is continuous & (- f) | X is continuous ) )
assume that
A1: X c= dom f and
A2: f | X is continuous ; :: thesis: ( ||.f.|| | X is continuous & (- f) | X is continuous )
thus ||.f.|| | X is continuous :: thesis: (- f) | X is continuous

proof

let r be Real; :: according to FCONT_1:def 2 :: thesis: ( not r in dom (||.f.|| | X) or ||.f.|| | X is_continuous_in r )
assume A3: r in dom (||.f.|| | X) ; :: thesis: ||.f.|| | X is_continuous_in r
then A4: ( r in dom ||.f.|| & r in X ) by RELAT_1:57;
then r in dom f by NORMSP_0:def 3;
then A5: r in dom (f | X) by A4, RELAT_1:57;
then A6: f | X is_continuous_in r by A2;
thus ||.f.|| | X is_continuous_in r :: thesis: verum

proof

let s1 be Real_Sequence; :: according to FCONT_1:def 1 :: thesis: ( not rng s1 c= dom (||.f.|| | X) or not s1 is convergent or not lim s1 = r or ( (||.f.|| | X) /* s1 is convergent & (||.f.|| | X) . r = lim ((||.f.|| | X) /* s1) ) )
assume that
A7: rng s1 c= dom (||.f.|| | X) and
A8: ( s1 is convergent & lim s1 = r ) ; :: thesis: ( (||.f.|| | X) /* s1 is convergent & (||.f.|| | X) . r = lim ((||.f.|| | X) /* s1) )
rng s1 c= (dom ||.f.||) /\ X by A7, RELAT_1:61;
then rng s1 c= (dom f) /\ X by NORMSP_0:def 3;
then A9: rng s1 c= dom (f | X) by RELAT_1:61;

now :: thesis: for n being Element of NAT holds ||.((f | X) /* s1).|| . n = ((||.f.|| | X) /* s1) . n

let n be Element of NAT ; :: thesis: ||.((f | X) /* s1).|| . n = ((||.f.|| | X) /* s1) . n
A10: s1 . n in rng s1 by VALUED_0:28;
then s1 . n in dom (f | X) by A9;
then s1 . n in (dom f) /\ X by RELAT_1:61;
then A11: ( s1 . n in X & s1 . n in dom f ) by XBOOLE_0:def 4;
then A12: s1 . n in dom ||.f.|| by NORMSP_0:def 3;
thus ||.((f | X) /* s1).|| . n = ||.(((f | X) /* s1) . n).|| by NORMSP_0:def 4
.= ||.((f | X) /. (s1 . n)).|| by A9, FUNCT_2:109
.= ||.(f /. (s1 . n)).|| by A9, A10, PARTFUN2:15
.= ||.f.|| . (s1 . n) by A12, NORMSP_0:def 3
.= (||.f.|| | X) . (s1 . n) by A11, FUNCT_1:49
.= ((||.f.|| | X) /* s1) . n by A7, FUNCT_2:108 ; :: thesis: verum

end;

then A13: ||.((f | X) /* s1).|| = (||.f.|| | X) /* s1 by FUNCT_2:63;
r in REAL by XREAL_0:def 1;
then A14: ||.((f | X) /. r).|| = ||.(f /. r).|| by A5, PARTFUN2:15
.= ||.f.|| . r by A4, NORMSP_0:def 3
.= (||.f.|| | X) . r by A3, FUNCT_1:47 ;
A15: (f | X) /* s1 is convergent by A6, A8, A9;
hence (||.f.|| | X) /* s1 is convergent by A13, NORMSP_1:23; :: thesis: (||.f.|| | X) . r = lim ((||.f.|| | X) /* s1)
(f | X) /. r = lim ((f | X) /* s1) by A6, A8, A9;
hence (||.f.|| | X) . r = lim ((||.f.|| | X) /* s1) by A15, A13, A14, LOPBAN_1:20; :: thesis: verum

end;

end;

((- 1) (#) f) | X is continuous by A1, A2, Th21;
hence (- f) | X is continuous by VFUNCT_1:23; :: thesis: verum