let X, Y be set ; for C being non empty set
for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
let C be non empty set ; for V being RealNormSpace
for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
let V be RealNormSpace; for f1, f2 being PartFunc of C,V 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 C,V; ( 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
- f2 is_bounded_on Y
by A2, Th45;
then
f1 + (- f2) is_bounded_on X /\ Y
by A1, Th46;
hence
f1 - f2 is_bounded_on X /\ Y
by Th25; verum