let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS st f is_continuous_on X holds
( ||.f.|| is_continuous_on X & - f is_continuous_on X )
let RNS be RealNormSpace; :: thesis: for X being set
for f being PartFunc of RNS,CNS st f is_continuous_on X holds
( ||.f.|| is_continuous_on X & - f is_continuous_on X )
let X be set ; :: thesis: for f being PartFunc of RNS,CNS st f is_continuous_on X holds
( ||.f.|| is_continuous_on X & - f is_continuous_on X )
let f be PartFunc of RNS,CNS; :: thesis: ( f is_continuous_on X implies ( ||.f.|| is_continuous_on X & - f is_continuous_on X ) )
assume A1: f is_continuous_on X ; :: thesis: ( ||.f.|| is_continuous_on X & - f is_continuous_on X )
thus ||.f.|| is_continuous_on X :: thesis: - f is_continuous_on X
proof
A2: X c= dom f by A1;
hence A3: X c= dom ||.f.|| by NORMSP_0:def 3; :: according to NFCONT_1:def 8 :: thesis: for b1 being Element of the carrier of RNS holds
( not b1 in X or ||.f.|| | X is_continuous_in b1 )
let r be Point of RNS; :: thesis: ( not r in X or ||.f.|| | X is_continuous_in r )
assume A4: r in X ; :: thesis: ||.f.|| | X is_continuous_in r
then A5: f | X is_continuous_in r by A1;
thus ||.f.|| | X is_continuous_in r :: thesis: verum
proof
A6: r in (dom ||.f.||) /\ X by A3, A4, XBOOLE_0:def 4;
hence r in dom (||.f.|| | X) by RELAT_1:61; :: according to NFCONT_1:def 6 :: thesis: for b1 being Element of K16(K17(NAT, the carrier of RNS)) holds
( not rng b1 c= dom (||.f.|| | X) or not b1 is convergent or not lim b1 = r or ( (||.f.|| | X) /* b1 is convergent & (||.f.|| | X) /. r = lim ((||.f.|| | X) /* b1) ) )
let s1 be sequence of RNS; :: 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;
then A10: (f | X) /. r = lim ((f | X) /* s1) by A5, A8;
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
dom s1 = NAT by FUNCT_2:def 1;
then A11: s1 . n in rng s1 by FUNCT_1:3;
then s1 . n in dom (f | X) by A9;
then A12: s1 . n in (dom f) /\ X by RELAT_1:61;
then A13: s1 . n in X by XBOOLE_0:def 4;
s1 . n in dom f by A12, XBOOLE_0:def 4;
then A14: 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, A11, PARTFUN2:15
.= ||.f.|| . (s1 . n) by A14, NORMSP_0:def 3
.= (||.f.|| | X) . (s1 . n) by A13, FUNCT_1:49
.= (||.f.|| | X) /. (s1 . n) by A7, A11, PARTFUN1:def 6
.= ((||.f.|| | X) /* s1) . n by A7, FUNCT_2:109 ; :: thesis: verum
end;
then A15: ||.((f | X) /* s1).|| = (||.f.|| | X) /* s1 by FUNCT_2:63;
A16: (f | X) /* s1 is convergent by A5, A8, A9;
hence (||.f.|| | X) /* s1 is convergent by A15, CLVECT_1:117; :: thesis: (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1)
||.((f | X) /. r).|| = ||.(f /. r).|| by A2, A4, PARTFUN2:17
.= ||.f.|| . r by A3, A4, NORMSP_0:def 3
.= ||.f.|| /. r by A3, A4, PARTFUN1:def 6
.= (||.f.|| | X) /. r by A6, PARTFUN2:16 ;
hence (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1) by A16, A10, A15, CLOPBAN1:19; :: thesis: verum
end;
end;
(- 1r) (#) f is_continuous_on X by A1, Th70;
hence - f is_continuous_on X by VFUNCT_2:23; :: thesis: verum