let Y be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
( |.f.| | Y is constant & (- f) | Y is constant )
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX st f | Y is constant holds
( |.f.| | Y is constant & (- f) | Y is constant )
let f be PartFunc of C,COMPLEX; :: 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 Element of COMPLEX such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
reconsider rr = |.r.| as Element of REAL by XREAL_0:def 1;

now :: thesis: for c being Element of C st c in Y /\ (dom |.f.|) holds
|.f.| . c = rr

let c be Element of C; :: thesis: ( c in Y /\ (dom |.f.|) implies |.f.| . c = rr )
assume A2: c in Y /\ (dom |.f.|) ; :: thesis: |.f.| . c = rr
then c in dom |.f.| by XBOOLE_0:def 4;
then A3: c in dom f by VALUED_1:def 11;
c in Y by A2, XBOOLE_0:def 4;
then A4: c in Y /\ (dom f) by A3, XBOOLE_0:def 4;
f . c = f /. c by A3, PARTFUN1:def 6;
hence |.f.| . c = |.(f /. c).| by VALUED_1:18
.= rr by A1, A4 ;
:: thesis: verum

end;

hence |.f.| | Y is constant by PARTFUN2:57; :: thesis: (- f) | Y is constant
A5: - r in COMPLEX by XCMPLX_0:def 2;

now :: thesis: for c being Element of C st c in Y /\ (dom (- f)) holds
(- f) /. c = - r

let c be Element of C; :: thesis: ( c in Y /\ (dom (- f)) implies (- f) /. c = - r )
assume A6: c in Y /\ (dom (- f)) ; :: thesis: (- f) /. c = - r
then c in Y /\ (dom f) by Th5;
then A7: - (f /. c) = - r by A1;
c in dom (- f) by A6, XBOOLE_0:def 4;
hence (- f) /. c = - r by A7, Th5; :: thesis: verum

end;

hence (- f) | Y is constant by A5, PARTFUN2:35; :: thesis: verum