for Y being set
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() )