let Y be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is bounded holds
( |.f.| | Y is bounded & (- f) | Y is bounded )
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX st f | Y is bounded holds
( |.f.| | Y is bounded & (- f) | Y is bounded )
let f be PartFunc of C,COMPLEX; :: thesis: ( f | Y is bounded implies ( |.f.| | Y is bounded & (- f) | Y is bounded ) )
assume A1: f | Y is bounded ; :: thesis: ( |.f.| | Y is bounded & (- f) | Y is bounded )
|.f.| | Y = |.(f | Y).| by RFUNCT_1:46;
hence |.f.| | Y is bounded by A1, Lm3; :: thesis: (- f) | Y is bounded
thus (- f) | Y is bounded by A1, Th71; :: thesis: verum