let n be Element of NAT ; :: thesis: for X being set

for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds

( |.f.| | X is continuous & (- f) | X is continuous )

let X be set ; :: thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds

( |.f.| | X is continuous & (- f) | X is continuous )

let f be PartFunc of REAL,(REAL n); :: thesis: ( X c= dom f & f | X is continuous implies ( |.f.| | X is continuous & (- f) | X is continuous ) )

assume A1: ( X c= dom f & f | X is continuous ) ; :: thesis: ( |.f.| | X is continuous & (- f) | X is continuous )

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

g | X is continuous by A1, Th23;

then A2: ( ||.g.|| | X is continuous & (- g) | X is continuous ) by A1, NFCONT_3:22;

hence |.f.| | X is continuous by Th9; :: thesis: (- f) | X is continuous

- g = - f by Th8;

hence (- f) | X is continuous by A2, Th23; :: thesis: verum

for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds

( |.f.| | X is continuous & (- f) | X is continuous )

let X be set ; :: thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds

( |.f.| | X is continuous & (- f) | X is continuous )

let f be PartFunc of REAL,(REAL n); :: thesis: ( X c= dom f & f | X is continuous implies ( |.f.| | X is continuous & (- f) | X is continuous ) )

assume A1: ( X c= dom f & f | X is continuous ) ; :: thesis: ( |.f.| | X is continuous & (- f) | X is continuous )

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

g | X is continuous by A1, Th23;

then A2: ( ||.g.|| | X is continuous & (- g) | X is continuous ) by A1, NFCONT_3:22;

hence |.f.| | X is continuous by Th9; :: thesis: (- f) | X is continuous

- g = - f by Th8;

hence (- f) | X is continuous by A2, Th23; :: thesis: verum