let T be non empty TopSpace; :: thesis: for f being Function of T,R^1
for r being positive real number 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 number 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 number ; :: 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

let x be set ; :: 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 abs (f . x) <= r by A2, Def1;
then 2 * (abs (f . x)) <= 2 * r by XREAL_1:66;
then (abs 2) * (abs (f . x)) <= 2 * r by ABSVALUE:def 1;
then (abs (- 2)) * (abs (f . x)) <= 2 * r by COMPLEX1:138;
then abs ((- 2) * (f . x)) <= r - (- r) by COMPLEX1:151;
then abs (((- r) + r) - (2 * (f . x))) <= r - (- r) ;
then f . x in [.(- r),r.] by RCOMP_1:9;
hence f . x in the carrier of (Closed-Interval-TSpace (- r),r) by TOPMETR:25; :: thesis: verum

end;

hence f is Function of T,(Closed-Interval-TSpace (- r),r) by A1, FUNCT_2:5; :: 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 abs (f . x) <= r )
assume x in the carrier of T /\ (dom f) ; :: thesis: abs (f . x) <= r
then f . x in the carrier of (Closed-Interval-TSpace (- r),r) by A3, FUNCT_2:7;
then f . x in [.(- r),r.] by TOPMETR:25;
then abs (((- r) + r) - (2 * (f . x))) <= r - (- r) by RCOMP_1:9;
then abs ((- 2) * (f . x)) <= r - (- r) ;
then (abs (- 2)) * (abs (f . x)) <= 2 * r by COMPLEX1:151;
then (abs 2) * (abs (f . x)) <= 2 * r by COMPLEX1:138;
then 2 * (abs (f . x)) <= 2 * r by ABSVALUE:def 1;
then (2 * (abs (f . x))) / 2 <= (2 * r) / 2 by XREAL_1:74;
hence abs (f . x) <= r ; :: thesis: verum