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;

now

let c be Element of C; :: thesis: ( c in Y /\ (dom |.f.|) implies |.f.| . c = |.r.| )
assume A2: c in Y /\ (dom |.f.|) ; :: thesis: |.f.| . c = |.r.|
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
.= |.r.| by A1, A4 ;
:: thesis: verum

end;

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

now

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

end;

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