let X, Y be set ; :: thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let V be RealNormSpace; :: thesis: for f being PartFunc of C,the carrier of V st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y
let f be PartFunc of C,the carrier of V; :: thesis: ( f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y )
assume A1: ( f is_bounded_on X & f is_bounded_on Y ) ; :: thesis: f is_bounded_on X \/ Y
then consider r1 being Real such that
A2: for c being Element of C st c in X /\ (dom f) holds
||.(f /. c).|| <= r1 by Def7;
consider r2 being Real such that
A3: for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r2 by A1, Def7;
take r = (abs r1) + (abs r2); :: according to VFUNCT_1:def 7 :: thesis: for c being Element of C st c in (X \/ Y) /\ (dom f) holds
||.(f /. c).|| <= r
let c be Element of C; :: thesis: ( c in (X \/ Y) /\ (dom f) implies ||.(f /. c).|| <= r )
assume c in (X \/ Y) /\ (dom f) ; :: thesis: ||.(f /. c).|| <= r
then A4: ( c in X \/ Y & c in dom f ) by XBOOLE_0:def 4;

now

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

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

then c in X /\ (dom f) by A4, XBOOLE_0:def 4;
then A5: ||.(f /. c).|| <= r1 by A2;
r1 <= abs r1 by ABSVALUE:11;
then A6: ||.(f /. c).|| <= abs r1 by A5, XXREAL_0:2;
0 <= abs r2 by COMPLEX1:132;
then ||.(f /. c).|| + 0 <= r by A6, XREAL_1:9;
hence ||.(f /. c).|| <= r ; :: thesis: verum

end;

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

then c in Y /\ (dom f) by A4, XBOOLE_0:def 4;
then A7: ||.(f /. c).|| <= r2 by A3;
r2 <= abs r2 by ABSVALUE:11;
then A8: ||.(f /. c).|| <= abs r2 by A7, XXREAL_0:2;
0 <= abs r1 by COMPLEX1:132;
then 0 + ||.(f /. c).|| <= r by A8, XREAL_1:9;
hence ||.(f /. c).|| <= r ; :: thesis: verum

end;

end;

end;

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