let CNS1, CNS2 be ComplexNormSpace; :: thesis: for X being set
for f being PartFunc of CNS1,CNS2 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 CNS1,CNS2 st f is_continuous_on X holds
( ||.f.|| is_continuous_on X & - f is_continuous_on X )
let f be PartFunc of CNS1,CNS2; :: 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, Def21;
hence A3: X c= dom ||.f.|| by Def2; :: according to NCFCONT1:def 25 :: thesis: for x0 being Point of CNS1 st x0 in X holds
||.f.|| | X is_continuous_in x0
let r be Point of CNS1; :: thesis: ( r in X implies ||.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, Def21;
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:90; :: according to NCFCONT1:def 19 :: thesis: for seq being sequence of CNS1 st rng seq c= dom (||.f.|| | X) & seq is convergent & lim seq = r holds
( (||.f.|| | X) /* seq is convergent & (||.f.|| | X) /. r = lim ((||.f.|| | X) /* seq) )
let s1 be sequence of CNS1; :: thesis: ( rng s1 c= dom (||.f.|| | X) & s1 is convergent & lim s1 = r implies ( (||.f.|| | X) /* s1 is convergent & (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1) ) )
assume A7: ( rng s1 c= dom (||.f.|| | X) & s1 is convergent & lim s1 = r ) ; :: thesis: ( (||.f.|| | X) /* s1 is convergent & (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1) )
then rng s1 c= (dom ||.f.||) /\ X by RELAT_1:90;
then rng s1 c= (dom f) /\ X by Def2;
then A8: rng s1 c= dom (f | X) by RELAT_1:90;
then A9: ( (f | X) /* s1 is convergent & (f | X) /. r = lim ((f | X) /* s1) ) by A5, A7, Def15;

now

let n be Element of NAT ; :: thesis: ||.((f | X) /* s1).|| . n = ((||.f.|| | X) /* s1) . n
dom s1 = NAT by FUNCT_2:def 1;
then A10: s1 . n in rng s1 by FUNCT_1:12;
then s1 . n in dom (f | X) by A8;
then s1 . n in (dom f) /\ X by RELAT_1:90;
then A11: ( s1 . n in dom f & s1 . n in X ) by XBOOLE_0:def 4;
then A12: ( s1 . n in dom ||.f.|| & s1 . n in X ) by Def2;
thus ||.((f | X) /* s1).|| . n = ||.(((f | X) /* s1) . n).|| by CLVECT_1:def 17
.= ||.((f | X) /. (s1 . n)).|| by A8, FUNCT_2:186
.= ||.(f /. (s1 . n)).|| by A8, A10, PARTFUN2:32
.= ||.f.|| . (s1 . n) by A12, Def2
.= (||.f.|| | X) . (s1 . n) by A11, FUNCT_1:72
.= (||.f.|| | X) /. (s1 . n) by A7, A10, PARTFUN1:def 8
.= ((||.f.|| | X) /* s1) . n by A7, FUNCT_2:186 ; :: thesis: verum

end;

then A13: ||.((f | X) /* s1).|| = (||.f.|| | X) /* s1 by FUNCT_2:113;
hence (||.f.|| | X) /* s1 is convergent by A9, CLVECT_1:119; :: thesis: (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1)
||.((f | X) /. r).|| = ||.(f /. r).|| by A2, A4, PARTFUN2:35
.= ||.f.|| . r by A3, A4, Def2
.= ||.f.|| /. r by A3, A4, PARTFUN1:def 8
.= (||.f.|| | X) /. r by A6, PARTFUN2:34 ;
hence (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1) by A9, A13, CLOPBAN1:22; :: thesis: verum

end;

end;

(- 1r ) (#) f is_continuous_on X by A1, Th89;
hence - f is_continuous_on X by VFUNCT_2:23; :: thesis: verum