let M be non empty set ; for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
let V be ComplexNormSpace; for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
let f1, f2 be PartFunc of M,V; for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
let X, Y be set ; ( f1 is_bounded_on X & f2 is_bounded_on Y implies f1 + f2 is_bounded_on X /\ Y )
assume that
A1:
f1 is_bounded_on X
and
A2:
f2 is_bounded_on Y
; f1 + f2 is_bounded_on X /\ Y
consider r1 being Real such that
A3:
for c being Element of M st c in X /\ (dom f1) holds
||.(f1 /. c).|| <= r1
by A1;
consider r2 being Real such that
A4:
for c being Element of M st c in Y /\ (dom f2) holds
||.(f2 /. c).|| <= r2
by A2;
take r = r1 + r2; VFUNCT_2:def 3 for x being Element of M st x in (X /\ Y) /\ (dom (f1 + f2)) holds
||.((f1 + f2) /. x).|| <= r
let c be Element of M; ( c in (X /\ Y) /\ (dom (f1 + f2)) implies ||.((f1 + f2) /. c).|| <= r )
assume A5:
c in (X /\ Y) /\ (dom (f1 + f2))
; ||.((f1 + f2) /. c).|| <= r
then A6:
c in X /\ Y
by XBOOLE_0:def 4;
then A7:
c in Y
by XBOOLE_0:def 4;
A8:
c in dom (f1 + f2)
by A5, XBOOLE_0:def 4;
then A9:
c in (dom f1) /\ (dom f2)
by VFUNCT_1:def 1;
then
c in dom f2
by XBOOLE_0:def 4;
then
c in Y /\ (dom f2)
by A7, XBOOLE_0:def 4;
then A10:
||.(f2 /. c).|| <= r2
by A4;
A11:
c in X
by A6, XBOOLE_0:def 4;
c in dom f1
by A9, XBOOLE_0:def 4;
then
c in X /\ (dom f1)
by A11, XBOOLE_0:def 4;
then
||.(f1 /. c).|| <= r1
by A3;
then
( ||.((f1 /. c) + (f2 /. c)).|| <= ||.(f1 /. c).|| + ||.(f2 /. c).|| & ||.(f1 /. c).|| + ||.(f2 /. c).|| <= r )
by A10, CLVECT_1:def 13, XREAL_1:7;
then
||.((f1 /. c) + (f2 /. c)).|| <= r
by XXREAL_0:2;
hence
||.((f1 + f2) /. c).|| <= r
by A8, VFUNCT_1:def 1; verum