let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,the carrier of V
for Y being set st f | Y is constant holds
( ||.f.|| | Y is constant & (- f) | Y is constant )
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,the carrier of V
for Y being set st f | Y is constant holds
( ||.f.|| | Y is constant & (- f) | Y is constant )
let f be PartFunc of M,the carrier of V; :: thesis: for Y being set st f | Y is constant holds
( ||.f.|| | Y is constant & (- f) | Y is constant )
let Y be set ; :: thesis: ( f | Y is constant implies ( ||.f.|| | Y is constant & (- f) | Y is constant ) )
assume f | Y is constant ; :: thesis: ( ||.f.|| | Y is constant & (- f) | Y is constant )
then consider r being VECTOR of V such that
A1: for c being Element of M st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:54;

now

let c be Element of M; :: thesis: ( c in Y /\ (dom ||.f.||) implies ||.f.|| . c = ||.r.|| )
assume c in Y /\ (dom ||.f.||) ; :: thesis: ||.f.|| . c = ||.r.||
then A2: ( c in dom ||.f.|| & c in Y ) by XBOOLE_0:def 4;
then c in dom f by Def5;
then A3: c in Y /\ (dom f) by A2, XBOOLE_0:def 4;
thus ||.f.|| . c = ||.(f /. c).|| by A2, Def5
.= ||.r.|| by A1, A3 ; :: thesis: verum

end;

hence ||.f.|| | Y is constant by PARTFUN2:76; :: thesis: (- f) | Y is constant

now

take p = - r; :: thesis: for c being Element of M st c in Y /\ (dom (- f)) holds
(- f) /. c = p
let c be Element of M; :: thesis: ( c in Y /\ (dom (- f)) implies (- f) /. c = p )
assume A4: c in Y /\ (dom (- f)) ; :: thesis: (- f) /. c = p
then c in Y /\ (dom f) by Def6;
then A5: - (f /. c) = p by A1;
c in dom (- f) by A4, XBOOLE_0:def 4;
hence (- f) /. c = p by A5, Def6; :: thesis: verum

end;

hence (- f) | Y is constant by PARTFUN2:54; :: thesis: verum