let T be non empty TopSpace; :: thesis: for f being Function of T,R^1
for r being positive Real holds
( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) )
let f be Function of T,R^1; :: thesis: for r being positive Real holds
( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) )
let r be positive Real; :: thesis: ( f, the carrier of T is_absolutely_bounded_by r iff f is Function of T,(Closed-Interval-TSpace ((- r),r)) )
A1: dom f = the carrier of T by FUNCT_2:def 1;
thus ( f, the carrier of T is_absolutely_bounded_by r implies f is Function of T,(Closed-Interval-TSpace ((- r),r)) ) :: thesis: ( f is Function of T,(Closed-Interval-TSpace ((- r),r)) implies f, the carrier of T is_absolutely_bounded_by r )
proof
assume A2: f, the carrier of T is_absolutely_bounded_by r ; :: thesis: f is Function of T,(Closed-Interval-TSpace ((- r),r))
now :: thesis: for x being object st x in the carrier of T holds
f . x in the carrier of (Closed-Interval-TSpace ((- r),r))
let x be object ; :: thesis: ( x in the carrier of T implies f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) )
assume x in the carrier of T ; :: thesis: f . x in the carrier of (Closed-Interval-TSpace ((- r),r))
then x in the carrier of T /\ (dom f) by A1;
then |.(f . x).| <= r by A2;
then 2 * |.(f . x).| <= 2 * r by XREAL_1:64;
then |.2.| * |.(f . x).| <= 2 * r by ABSVALUE:def 1;
then |.(- 2).| * |.(f . x).| <= 2 * r by COMPLEX1:52;
then |.((- 2) * (f . x)).| <= r - (- r) by COMPLEX1:65;
then |.(((- r) + r) - (2 * (f . x))).| <= r - (- r) ;
then f . x in [.(- r),r.] by RCOMP_1:2;
hence f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) by TOPMETR:18; :: thesis: verum
end;
hence f is Function of T,(Closed-Interval-TSpace ((- r),r)) by A1, FUNCT_2:3; :: thesis: verum
end;
assume A3: f is Function of T,(Closed-Interval-TSpace ((- r),r)) ; :: thesis: f, the carrier of T is_absolutely_bounded_by r
let x be set ; :: according to TIETZE:def 1 :: thesis: ( x in the carrier of T /\ (dom f) implies |.(f . x).| <= r )
assume x in the carrier of T /\ (dom f) ; :: thesis: |.(f . x).| <= r
then f . x in the carrier of (Closed-Interval-TSpace ((- r),r)) by A3, FUNCT_2:5;
then f . x in [.(- r),r.] by TOPMETR:18;
then |.(((- r) + r) - (2 * (f . x))).| <= r - (- r) by RCOMP_1:2;
then |.((- 2) * (f . x)).| <= r - (- r) ;
then |.(- 2).| * |.(f . x).| <= 2 * r by COMPLEX1:65;
then |.2.| * |.(f . x).| <= 2 * r by COMPLEX1:52;
then 2 * |.(f . x).| <= 2 * r by ABSVALUE:def 1;
then (2 * |.(f . x).|) / 2 <= (2 * r) / 2 by XREAL_1:72;
hence |.(f . x).| <= r ; :: thesis: verum