let Y be set ; :: thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
( ||.f.|| | Y is V8() & (- f) | Y is V8() )
let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V st f | Y is V8() holds
( ||.f.|| | Y is V8() & (- f) | Y is V8() )
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V st f | Y is V8() holds
( ||.f.|| | Y is V8() & (- f) | Y is V8() )
let f be PartFunc of C,V; :: thesis: ( f | Y is V8() implies ( ||.f.|| | Y is V8() & (- f) | Y is V8() ) )
assume f | Y is V8() ; :: thesis: ( ||.f.|| | Y is V8() & (- f) | Y is V8() )
then consider r being VECTOR of V such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
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 A2: c in Y /\ (dom ||.f.||) ; :: thesis: ||.f.|| . c = ||.r.||
then A3: c in Y by XBOOLE_0:def 4;
A4: c in dom ||.f.|| by A2, XBOOLE_0:def 4;
then c in dom f by NORMSP_0:def 3;
then A5: c in Y /\ (dom f) by A3, XBOOLE_0:def 4;
thus ||.f.|| . c = ||.(f /. c).|| by A4, NORMSP_0:def 3
.= ||.r.|| by A1, A5 ; :: thesis: verum
end;
hence ||.f.|| | Y is V8() by PARTFUN2:57; :: thesis: (- f) | Y is V8()
now :: thesis: ex p being Element of the U1 of V st
for c being Element of C st c in Y /\ (dom (- f)) holds
(- f) /. c = p
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 A6: c in Y /\ (dom (- f)) ; :: thesis: (- f) /. c = p
then c in Y /\ (dom f) by Def5;
then A7: - (f /. c) = p by A1;
c in dom (- f) by A6, XBOOLE_0:def 4;
hence (- f) /. c = p by A7, Def5; :: thesis: verum
end;
hence (- f) | Y is V8() by PARTFUN2:35; :: thesis: verum