let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for X, Y being set st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for X, Y being set st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let f be PartFunc of M,V; :: thesis: for X, Y being set st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let X, Y be set ; :: thesis: ( f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y )
assume that
A1: f is_bounded_on X and
A2: f is_bounded_on Y ; :: thesis: f is_bounded_on X \/ Y
consider r1 being Real such that
A3: for c being Element of M st c in X /\ (dom f) holds
||.(f /. c).|| <= r1 by A1;
consider r2 being Real such that
A4: for c being Element of M st c in Y /\ (dom f) holds
||.(f /. c).|| <= r2 by A2;
reconsider r = |.r1.| + |.r2.| as Real ;
take r ; :: according to VFUNCT_2:def 3 :: thesis: for x being Element of M st x in (X \/ Y) /\ (dom f) holds
||.(f /. x).|| <= r
let c be Element of M; :: thesis: ( c in (X \/ Y) /\ (dom f) implies ||.(f /. c).|| <= r )
assume A5: c in (X \/ Y) /\ (dom f) ; :: thesis: ||.(f /. c).|| <= r
then A6: c in dom f by XBOOLE_0:def 4;
A7: c in X \/ Y by A5, XBOOLE_0:def 4;

now :: thesis: ||.(f /. c).|| <= r

per cases ( c in X or c in Y ) by A7, XBOOLE_0:def 3;

suppose c in X ; :: thesis: ||.(f /. c).|| <= r

then c in X /\ (dom f) by A6, XBOOLE_0:def 4;
then A8: ||.(f /. c).|| <= r1 by A3;
A9: 0 <= |.r2.| by COMPLEX1:46;
r1 <= |.r1.| by ABSVALUE:4;
then ||.(f /. c).|| <= |.r1.| by A8, XXREAL_0:2;
then ||.(f /. c).|| + 0 <= r by A9, XREAL_1:7;
hence ||.(f /. c).|| <= r ; :: thesis: verum

end;

suppose c in Y ; :: thesis: ||.(f /. c).|| <= r

then c in Y /\ (dom f) by A6, XBOOLE_0:def 4;
then A10: ||.(f /. c).|| <= r2 by A4;
A11: 0 <= |.r1.| by COMPLEX1:46;
r2 <= |.r2.| by ABSVALUE:4;
then ||.(f /. c).|| <= |.r2.| by A10, XXREAL_0:2;
then 0 + ||.(f /. c).|| <= r by A11, XREAL_1:7;
hence ||.(f /. c).|| <= r ; :: thesis: verum

end;

end;

end;

hence ||.(f /. c).|| <= r ; :: thesis: verum