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