let S, T be RealNormSpace; :: thesis: for h being PartFunc of S,T
for seq being sequence of S st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )
let h be PartFunc of S,T; :: thesis: for seq being sequence of S st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )
let seq be sequence of S; :: 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 Th6;
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) = (- jj) * (h /* seq) by Th2
.= ((- 1) (#) h) /* seq by A1, Th13
.= (- h) /* seq by VFUNCT_1:23 ; :: thesis: verum