let X, Y be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
let f be PartFunc of C,COMPLEX; :: thesis: ( f | X is bounded & f | Y is bounded implies f | (X \/ Y) is bounded )
assume that
A1: f | X is bounded and
A2: f | Y is bounded ; :: thesis: f | (X \/ Y) is bounded
|.f.| | Y = |.(f | Y).| by RFUNCT_1:46;
then A3: |.f.| | Y is bounded by A2, Lm3;
|.f.| | X = |.(f | X).| by RFUNCT_1:46;
then |.f.| | X is bounded by A1, Lm3;
then ( |.f.| | (X \/ Y) = |.(f | (X \/ Y)).| & |.f.| | (X \/ Y) is bounded ) by A3, RFUNCT_1:46, RFUNCT_1:87;
hence f | (X \/ Y) is bounded by Lm3; :: thesis: verum