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 )
F: |.f.| | Y = |.(f | Y).| by RFUNCT_1:62;
G: |.f.| | X = |.(f | X).| by RFUNCT_1:62;
H: |.f.| | (X \/ Y) = |.(f | (X \/ Y)).| by RFUNCT_1:62;
assume A1: ( f | X is bounded & f | Y is bounded ) ; :: thesis: f | (X \/ Y) is bounded
then A2: |.f.| | X is bounded by Def3, G;
|.f.| | Y is bounded by A1, Def3, F;
then |.f.| | (X \/ Y) is bounded by A2, RFUNCT_1:104;
hence f | (X \/ Y) is bounded by Def3, H; :: thesis: verum