let CNS1, CNS2 be ComplexNormSpace; :: thesis: for h being PartFunc of CNS1,CNS2
for seq being sequence of CNS1 st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )
let h be PartFunc of CNS1,CNS2; :: thesis: for seq being sequence of CNS1 st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )
let seq be sequence of CNS1; :: thesis: ( rng seq c= dom h implies ( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq ) )
assume A1: rng seq c= dom h ; :: thesis: ( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )
then A2: rng seq c= dom ||.h.|| by NORMSP_0:def 3;

now :: thesis: for n being Element of NAT holds ||.(h /* seq).|| . n = (||.h.|| /* seq) . n

let n be Element of NAT ; :: thesis: ||.(h /* seq).|| . n = (||.h.|| /* seq) . n
seq . n in rng seq by Th7;
then seq . n in dom h by A1;
then A3: seq . n in dom ||.h.|| by NORMSP_0:def 3;
thus ||.(h /* seq).|| . n = ||.((h /* seq) . n).|| by NORMSP_0:def 4
.= ||.(h /. (seq . n)).|| by A1, FUNCT_2:109
.= ||.h.|| . (seq . n) by A3, NORMSP_0:def 3
.= ||.h.|| /. (seq . n) by A3, PARTFUN1:def 6
.= (||.h.|| /* seq) . n by A2, FUNCT_2:109 ; :: thesis: verum

end;

hence ||.(h /* seq).|| = ||.h.|| /* seq by FUNCT_2:63; :: thesis: - (h /* seq) = (- h) /* seq
thus - (h /* seq) = (- 1r) * (h /* seq) by Th1
.= ((- 1r) (#) h) /* seq by A1, Th26
.= (- h) /* seq by VFUNCT_2:23 ; :: thesis: verum