tops_4.miz



    begin

    reserve n,m for Nat,

T for non empty TopSpace,

M,M1,M2 for non empty MetrSpace;

    theorem :: TOPS_4:1

    

     Th1: for A,B,S,T be TopSpace, f be Function of A, S, g be Function of B, T st the TopStruct of A = the TopStruct of B & the TopStruct of S = the TopStruct of T & f = g & f is open holds g is open

    proof

      let A,B,S,T be TopSpace;

      let f be Function of A, S;

      let g be Function of B, T;

      assume that

       A1: the TopStruct of A = the TopStruct of B and

       A2: the TopStruct of S = the TopStruct of T and

       A3: f = g and

       A4: f is open;

      let b be Subset of B;

      assume

       A5: b is open;

      reconsider a = b as Subset of A by A1;

      a is open by A1, A5, TOPS_3: 76;

      then (f .: a) is open by A4;

      hence thesis by A2, A3, TOPS_3: 76;

    end;

    theorem :: TOPS_4:2

    for P be Subset of ( TOP-REAL m) holds P is open iff for p be Point of ( TOP-REAL m) st p in P holds ex r be positive Real st ( Ball (p,r)) c= P

    proof

      let P be Subset of ( TOP-REAL m);

      

       A1: the TopStruct of ( TOP-REAL m) = ( TopSpaceMetr ( Euclid m)) by EUCLID:def 8;

      then

      reconsider P1 = P as Subset of ( TopSpaceMetr ( Euclid m));

      hereby

        assume

         A2: P is open;

        let p be Point of ( TOP-REAL m);

        assume

         A3: p in P;

        reconsider e = p as Point of ( Euclid m) by EUCLID: 67;

        P1 is open by A2, A1, TOPS_3: 76;

        then

        consider r be Real such that

         A4: r > 0 and

         A5: ( Ball (e,r)) c= P1 by A3, TOPMETR: 15;

        reconsider r as positive Real by A4;

        take r;

        thus ( Ball (p,r)) c= P by A5, TOPREAL9: 13;

      end;

      assume

       A6: for p be Point of ( TOP-REAL m) st p in P holds ex r be positive Real st ( Ball (p,r)) c= P;

      for p be Point of ( Euclid m) st p in P1 holds ex r be Real st r > 0 & ( Ball (p,r)) c= P1

      proof

        let p be Point of ( Euclid m);

        assume

         A7: p in P1;

        reconsider e = p as Point of ( TOP-REAL m) by EUCLID: 67;

        consider r be positive Real such that

         A8: ( Ball (e,r)) c= P1 by A6, A7;

        take r;

        thus thesis by A8, TOPREAL9: 13;

      end;

      then P1 is open by TOPMETR: 15;

      hence thesis by A1, TOPS_3: 76;

    end;

    theorem :: TOPS_4:3

    

     Th3: for X,Y be non empty TopSpace, f be Function of X, Y holds f is open iff for p be Point of X, V be open Subset of X st p in V holds ex W be open Subset of Y st (f . p) in W & W c= (f .: V)

    proof

      let X,Y be non empty TopSpace, f be Function of X, Y;

      thus f is open implies for p be Point of X, V be open Subset of X st p in V holds ex W be open Subset of Y st (f . p) in W & W c= (f .: V)

      proof

        assume

         A1: f is open;

        let p be Point of X, V be open Subset of X such that

         A2: p in V;

        V is a_neighborhood of p by A2, CONNSP_2: 3;

        then

        consider W be open a_neighborhood of (f . p) such that

         A3: W c= (f .: V) by A1, TOPGRP_1: 22;

        take W;

        thus (f . p) in W by CONNSP_2: 4;

        thus thesis by A3;

      end;

      assume

       A4: for p be Point of X, V be open Subset of X st p in V holds ex W be open Subset of Y st (f . p) in W & W c= (f .: V);

      for p be Point of X, P be open a_neighborhood of p holds ex R be a_neighborhood of (f . p) st R c= (f .: P)

      proof

        let p be Point of X;

        let P be open a_neighborhood of p;

        consider W be open Subset of Y such that

         A5: (f . p) in W and

         A6: W c= (f .: P) by A4, CONNSP_2: 4;

        W is a_neighborhood of (f . p) by A5, CONNSP_2: 3;

        hence thesis by A6;

      end;

      hence thesis by TOPGRP_1: 23;

    end;

    theorem :: TOPS_4:4

    

     Th4: for f be Function of T, ( TopSpaceMetr M) holds f is open iff for p be Point of T, V be open Subset of T, q be Point of M st q = (f . p) & p in V holds ex r be positive Real st ( Ball (q,r)) c= (f .: V)

    proof

      let f be Function of T, ( TopSpaceMetr M);

      thus f is open implies for p be Point of T, V be open Subset of T, q be Point of M st q = (f . p) & p in V holds ex r be positive Real st ( Ball (q,r)) c= (f .: V)

      proof

        assume

         A1: f is open;

        let p be Point of T, V be open Subset of T, q be Point of M such that

         A2: q = (f . p);

        assume p in V;

        then

        consider W be open Subset of ( TopSpaceMetr M) such that

         A3: (f . p) in W and

         A4: W c= (f .: V) by A1, Th3;

        ex r be Real st r > 0 & ( Ball (q,r)) c= W by A2, A3, TOPMETR: 15;

        hence thesis by A4, XBOOLE_1: 1;

      end;

      assume

       A5: for p be Point of T, V be open Subset of T, q be Point of M st q = (f . p) & p in V holds ex r be positive Real st ( Ball (q,r)) c= (f .: V);

      for p be Point of T, V be open Subset of T st p in V holds ex W be open Subset of ( TopSpaceMetr M) st (f . p) in W & W c= (f .: V)

      proof

        let p be Point of T;

        let V be open Subset of T;

        reconsider q = (f . p) as Point of M;

        assume p in V;

        then

        consider r be positive Real such that

         A6: ( Ball (q,r)) c= (f .: V) by A5;

        reconsider W = ( Ball (q,r)) as open Subset of ( TopSpaceMetr M) by TOPMETR: 14;

        take W;

        thus (f . p) in W by GOBOARD6: 1;

        thus W c= (f .: V) by A6;

      end;

      hence thesis by Th3;

    end;

    theorem :: TOPS_4:5

    

     Th5: for f be Function of ( TopSpaceMetr M), T holds f is open iff for p be Point of M, r be positive Real holds ex W be open Subset of T st (f . p) in W & W c= (f .: ( Ball (p,r)))

    proof

      let f be Function of ( TopSpaceMetr M), T;

      hereby

        assume

         A1: f is open;

        let p be Point of M, r be positive Real;

        

         A2: p in ( Ball (p,r)) by GOBOARD6: 1;

        reconsider V = ( Ball (p,r)) as Subset of ( TopSpaceMetr M);

        V is open by TOPMETR: 14;

        then

        consider W be open Subset of T such that

         A3: (f . p) in W & W c= (f .: V) by A1, A2, Th3;

        take W;

        thus (f . p) in W & W c= (f .: ( Ball (p,r))) by A3;

      end;

      assume

       A4: for p be Point of M, r be positive Real holds ex W be open Subset of T st (f . p) in W & W c= (f .: ( Ball (p,r)));

      for p be Point of ( TopSpaceMetr M), V be open Subset of ( TopSpaceMetr M) st p in V holds ex W be open Subset of T st (f . p) in W & W c= (f .: V)

      proof

        let p be Point of ( TopSpaceMetr M);

        let V be open Subset of ( TopSpaceMetr M);

        reconsider q = p as Point of M;

        assume p in V;

        then

        consider r be Real such that

         A5: r > 0 and

         A6: ( Ball (q,r)) c= V by TOPMETR: 15;

        consider W be open Subset of T such that

         A7: (f . p) in W and

         A8: W c= (f .: ( Ball (q,r))) by A4, A5;

        take W;

        thus (f . p) in W by A7;

        (f .: ( Ball (q,r))) c= (f .: V) by A6, RELAT_1: 123;

        hence thesis by A8;

      end;

      hence thesis by Th3;

    end;

    theorem :: TOPS_4:6

    

     Th6: for f be Function of ( TopSpaceMetr M1), ( TopSpaceMetr M2) holds f is open iff for p be Point of M1, q be Point of M2, r be positive Real st q = (f . p) holds ex s be positive Real st ( Ball (q,s)) c= (f .: ( Ball (p,r)))

    proof

      let f be Function of ( TopSpaceMetr M1), ( TopSpaceMetr M2);

      thus f is open implies for p be Point of M1, q be Point of M2, r be positive Real st q = (f . p) holds ex s be positive Real st ( Ball (q,s)) c= (f .: ( Ball (p,r)))

      proof

        assume

         A1: f is open;

        let p be Point of M1, q be Point of M2, r be positive Real such that

         A2: q = (f . p);

        reconsider V = ( Ball (p,r)) as Subset of ( TopSpaceMetr M1);

        

         A3: p in V by GOBOARD6: 1;

        V is open by TOPMETR: 14;

        hence thesis by A1, A2, A3, Th4;

      end;

      assume

       A4: for p be Point of M1, q be Point of M2, r be positive Real st q = (f . p) holds ex s be positive Real st ( Ball (q,s)) c= (f .: ( Ball (p,r)));

      for p be Point of ( TopSpaceMetr M1), V be open Subset of ( TopSpaceMetr M1), q be Point of M2 st q = (f . p) & p in V holds ex r be positive Real st ( Ball (q,r)) c= (f .: V)

      proof

        let p be Point of ( TopSpaceMetr M1), V be open Subset of ( TopSpaceMetr M1), q be Point of M2 such that

         A5: q = (f . p);

        reconsider p1 = p as Point of M1;

        assume p in V;

        then

        consider r be Real such that

         A6: r > 0 and

         A7: ( Ball (p1,r)) c= V by TOPMETR: 15;

        

         A8: (f .: ( Ball (p1,r))) c= (f .: V) by A7, RELAT_1: 123;

        ex s be positive Real st ( Ball (q,s)) c= (f .: ( Ball (p1,r))) by A4, A5, A6;

        hence thesis by A8, XBOOLE_1: 1;

      end;

      hence thesis by Th4;

    end;

    theorem :: TOPS_4:7

    for f be Function of T, ( TOP-REAL m) holds f is open iff for p be Point of T, V be open Subset of T st p in V holds ex r be positive Real st ( Ball ((f . p),r)) c= (f .: V)

    proof

      let f be Function of T, ( TOP-REAL m);

      

       A1: the TopStruct of ( TOP-REAL m) = ( TopSpaceMetr ( Euclid m)) by EUCLID:def 8;

      then

      reconsider f1 = f as Function of T, ( TopSpaceMetr ( Euclid m));

      

       A2: the TopStruct of T = the TopStruct of T;

      thus f is open implies for p be Point of T, V be open Subset of T st p in V holds ex r be positive Real st ( Ball ((f . p),r)) c= (f .: V)

      proof

        assume

         A3: f is open;

        let p be Point of T, V be open Subset of T;

        assume

         A4: p in V;

        reconsider fp = (f . p) as Point of ( Euclid m) by EUCLID: 67;

        f1 is open by A3, A1, A2, Th1;

        then

        consider r be positive Real such that

         A5: ( Ball (fp,r)) c= (f1 .: V) by A4, Th4;

        ( Ball ((f . p),r)) = ( Ball (fp,r)) by TOPREAL9: 13;

        hence thesis by A5;

      end;

      assume

       A6: for p be Point of T, V be open Subset of T st p in V holds ex r be positive Real st ( Ball ((f . p),r)) c= (f .: V);

      for p be Point of T, V be open Subset of T, q be Point of ( Euclid m) st q = (f1 . p) & p in V holds ex r be positive Real st ( Ball (q,r)) c= (f1 .: V)

      proof

        let p be Point of T, V be open Subset of T, q be Point of ( Euclid m) such that

         A7: q = (f1 . p);

        assume p in V;

        then

        consider r be positive Real such that

         A8: ( Ball ((f . p),r)) c= (f .: V) by A6;

        ( Ball ((f . p),r)) = ( Ball (q,r)) by A7, TOPREAL9: 13;

        hence thesis by A8;

      end;

      then f1 is open by Th4;

      hence thesis by A1, A2, Th1;

    end;

    theorem :: TOPS_4:8

    for f be Function of ( TOP-REAL m), T holds f is open iff for p be Point of ( TOP-REAL m), r be positive Real holds ex W be open Subset of T st (f . p) in W & W c= (f .: ( Ball (p,r)))

    proof

      let f be Function of ( TOP-REAL m), T;

      

       A1: the TopStruct of ( TOP-REAL m) = ( TopSpaceMetr ( Euclid m)) by EUCLID:def 8;

      then

      reconsider f1 = f as Function of ( TopSpaceMetr ( Euclid m)), T;

      

       A2: the TopStruct of T = the TopStruct of T;

      thus f is open implies for p be Point of ( TOP-REAL m), r be positive Real holds ex W be open Subset of T st (f . p) in W & W c= (f .: ( Ball (p,r)))

      proof

        assume

         A3: f is open;

        let p be Point of ( TOP-REAL m), r be positive Real;

        reconsider q = p as Point of ( Euclid m) by EUCLID: 67;

        f1 is open by A3, A1, A2, Th1;

        then

        consider W be open Subset of T such that

         A4: (f1 . p) in W & W c= (f1 .: ( Ball (q,r))) by Th5;

        ( Ball (p,r)) = ( Ball (q,r)) by TOPREAL9: 13;

        hence thesis by A4;

      end;

      assume

       A5: for p be Point of ( TOP-REAL m), r be positive Real holds ex W be open Subset of T st (f . p) in W & W c= (f .: ( Ball (p,r)));

      for p be Point of ( Euclid m), r be positive Real holds ex W be open Subset of T st (f1 . p) in W & W c= (f1 .: ( Ball (p,r)))

      proof

        let p be Point of ( Euclid m), r be positive Real;

        reconsider q = p as Point of ( TOP-REAL m) by EUCLID: 67;

        consider W be open Subset of T such that

         A6: (f . q) in W & W c= (f .: ( Ball (q,r))) by A5;

        ( Ball (p,r)) = ( Ball (q,r)) by TOPREAL9: 13;

        hence thesis by A6;

      end;

      then f1 is open by Th5;

      hence thesis by A1, A2, Th1;

    end;

    theorem :: TOPS_4:9

    for f be Function of ( TOP-REAL m), ( TOP-REAL n) holds f is open iff for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st ( Ball ((f . p),s)) c= (f .: ( Ball (p,r)))

    proof

      let f be Function of ( TOP-REAL m), ( TOP-REAL n);

      

       A1: the TopStruct of ( TOP-REAL m) = ( TopSpaceMetr ( Euclid m)) & the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      then

      reconsider f1 = f as Function of ( TopSpaceMetr ( Euclid m)), ( TopSpaceMetr ( Euclid n));

      thus f is open implies for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st ( Ball ((f . p),s)) c= (f .: ( Ball (p,r)))

      proof

        assume

         A2: f is open;

        let p be Point of ( TOP-REAL m), r be positive Real;

        reconsider p1 = p as Point of ( Euclid m) by EUCLID: 67;

        reconsider q1 = (f . p) as Point of ( Euclid n) by EUCLID: 67;

        f1 is open by A1, A2, Th1;

        then

        consider s be positive Real such that

         A3: ( Ball (q1,s)) c= (f1 .: ( Ball (p1,r))) by Th6;

        ( Ball (p1,r)) = ( Ball (p,r)) & ( Ball (q1,s)) = ( Ball ((f . p),s)) by TOPREAL9: 13;

        hence thesis by A3;

      end;

      assume

       A4: for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st ( Ball ((f . p),s)) c= (f .: ( Ball (p,r)));

      for p be Point of ( Euclid m), q be Point of ( Euclid n), r be positive Real st q = (f1 . p) holds ex s be positive Real st ( Ball (q,s)) c= (f1 .: ( Ball (p,r)))

      proof

        let p be Point of ( Euclid m), q be Point of ( Euclid n), r be positive Real such that

         A5: q = (f1 . p);

        reconsider p1 = p as Point of ( TOP-REAL m) by EUCLID: 67;

        reconsider q1 = q as Point of ( TOP-REAL n) by EUCLID: 67;

        consider s be positive Real such that

         A6: ( Ball (q1,s)) c= (f .: ( Ball (p1,r))) by A4, A5;

        ( Ball (p1,r)) = ( Ball (p,r)) & ( Ball (q1,s)) = ( Ball (q,s)) by TOPREAL9: 13;

        hence thesis by A6;

      end;

      then f1 is open by Th6;

      hence thesis by A1, Th1;

    end;

    theorem :: TOPS_4:10

    for f be Function of T, R^1 holds f is open iff for p be Point of T, V be open Subset of T st p in V holds ex r be positive Real st ].((f . p) - r), ((f . p) + r).[ c= (f .: V)

    proof

      let f be Function of T, R^1 ;

      thus f is open implies for p be Point of T, V be open Subset of T st p in V holds ex r be positive Real st ].((f . p) - r), ((f . p) + r).[ c= (f .: V)

      proof

        assume

         A1: f is open;

        let p be Point of T, V be open Subset of T;

        assume

         A2: p in V;

        reconsider fp = (f . p) as Point of RealSpace ;

        consider r be positive Real such that

         A3: ( Ball (fp,r)) c= (f .: V) by A1, A2, Th4;

         ].(fp - r), (fp + r).[ = ( Ball (fp,r)) by FRECHET: 7;

        hence thesis by A3;

      end;

      assume

       A4: for p be Point of T, V be open Subset of T st p in V holds ex r be positive Real st ].((f . p) - r), ((f . p) + r).[ c= (f .: V);

      for p be Point of T, V be open Subset of T, q be Point of RealSpace st q = (f . p) & p in V holds ex r be positive Real st ( Ball (q,r)) c= (f .: V)

      proof

        let p be Point of T, V be open Subset of T, q be Point of RealSpace such that

         A5: q = (f . p);

        assume p in V;

        then

        consider r be positive Real such that

         A6: ].((f . p) - r), ((f . p) + r).[ c= (f .: V) by A4;

         ].(q - r), (q + r).[ = ( Ball (q,r)) by FRECHET: 7;

        hence thesis by A5, A6;

      end;

      hence thesis by Th4;

    end;

    theorem :: TOPS_4:11

    for f be Function of R^1 , T holds f is open iff for p be Point of R^1 , r be positive Real holds ex V be open Subset of T st (f . p) in V & V c= (f .: ].(p - r), (p + r).[)

    proof

      let f be Function of R^1 , T;

      thus f is open implies for p be Point of R^1 , r be positive Real holds ex W be open Subset of T st (f . p) in W & W c= (f .: ].(p - r), (p + r).[)

      proof

        assume

         A1: f is open;

        let p be Point of R^1 , r be positive Real;

        reconsider q = p as Point of RealSpace ;

        consider W be open Subset of T such that

         A2: (f . p) in W & W c= (f .: ( Ball (q,r))) by A1, Th5;

         ].(q - r), (q + r).[ = ( Ball (q,r)) by FRECHET: 7;

        hence thesis by A2;

      end;

      assume

       A3: for p be Point of R^1 , r be positive Real holds ex W be open Subset of T st (f . p) in W & W c= (f .: ].(p - r), (p + r).[);

      for p be Point of RealSpace , r be positive Real holds ex W be open Subset of T st (f . p) in W & W c= (f .: ( Ball (p,r)))

      proof

        let p be Point of RealSpace , r be positive Real;

        reconsider q = p as Point of R^1 ;

        consider W be open Subset of T such that

         A4: (f . q) in W & W c= (f .: ].(p - r), (p + r).[) by A3;

         ].(p - r), (p + r).[ = ( Ball (p,r)) by FRECHET: 7;

        hence thesis by A4;

      end;

      hence thesis by Th5;

    end;

    theorem :: TOPS_4:12

    for f be Function of R^1 , R^1 holds f is open iff for p be Point of R^1 , r be positive Real holds ex s be positive Real st ].((f . p) - s), ((f . p) + s).[ c= (f .: ].(p - r), (p + r).[)

    proof

      let f be Function of R^1 , R^1 ;

      thus f is open implies for p be Point of R^1 , r be positive Real holds ex s be positive Real st ].((f . p) - s), ((f . p) + s).[ c= (f .: ].(p - r), (p + r).[)

      proof

        assume

         A1: f is open;

        let p be Point of R^1 , r be positive Real;

        reconsider p1 = p, q1 = (f . p) as Point of RealSpace ;

        consider s be positive Real such that

         A2: ( Ball (q1,s)) c= (f .: ( Ball (p1,r))) by A1, Th6;

         ].(p - r), (p + r).[ = ( Ball (p1,r)) & ].((f . p) - s), ((f . p) + s).[ = ( Ball (q1,s)) by FRECHET: 7;

        hence thesis by A2;

      end;

      assume

       A3: for p be Point of R^1 , r be positive Real holds ex s be positive Real st ].((f . p) - s), ((f . p) + s).[ c= (f .: ].(p - r), (p + r).[);

      for p,q be Point of RealSpace , r be positive Real st q = (f . p) holds ex s be positive Real st ( Ball (q,s)) c= (f .: ( Ball (p,r)))

      proof

        let p,q be Point of RealSpace , r be positive Real such that

         A4: q = (f . p);

        consider s be positive Real such that

         A5: ].((f . p) - s), ((f . p) + s).[ c= (f .: ].(p - r), (p + r).[) by A3;

         ].(p - r), (p + r).[ = ( Ball (p,r)) & ].((f . p) - s), ((f . p) + s).[ = ( Ball (q,s)) by A4, FRECHET: 7;

        hence thesis by A5;

      end;

      hence thesis by Th6;

    end;

    theorem :: TOPS_4:13

    for f be Function of ( TOP-REAL m), R^1 holds f is open iff for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st ].((f . p) - s), ((f . p) + s).[ c= (f .: ( Ball (p,r)))

    proof

      let f be Function of ( TOP-REAL m), R^1 ;

      

       A1: m in NAT by ORDINAL1:def 12;

      hereby

        assume

         A2: f is open;

        let p be Point of ( TOP-REAL m), r be positive Real;

        p in ( Ball (p,r)) by A1, TOPGEN_5: 13;

        then

         A3: (f . p) in (f .: ( Ball (p,r))) by FUNCT_2: 35;

        (f .: ( Ball (p,r))) is open by A2;

        then

        consider s be Real such that

         A4: s > 0 and

         A5: ].((f . p) - s), ((f . p) + s).[ c= (f .: ( Ball (p,r))) by A3, FRECHET: 8;

        reconsider s as positive Real by A4;

        take s;

        thus ].((f . p) - s), ((f . p) + s).[ c= (f .: ( Ball (p,r))) by A5;

      end;

      assume

       A6: for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st ].((f . p) - s), ((f . p) + s).[ c= (f .: ( Ball (p,r)));

      let A be Subset of ( TOP-REAL m) such that

       A7: A is open;

      for x be set holds x in (f .: A) iff ex Q be Subset of R^1 st Q is open & Q c= (f .: A) & x in Q

      proof

        let x be set;

        hereby

          assume x in (f .: A);

          then

          consider p be Point of ( TOP-REAL m) such that

           A8: p in A and

           A9: x = (f . p) by FUNCT_2: 65;

          reconsider u = p as Point of ( Euclid m) by EUCLID: 67;

          A = ( Int A) by A7, TOPS_1: 23;

          then

          consider e be Real such that

           A10: e > 0 and

           A11: ( Ball (u,e)) c= A by A8, GOBOARD6: 5;

          

           A12: ( Ball (u,e)) = ( Ball (p,e)) by TOPREAL9: 13;

          consider s be positive Real such that

           A13: ].((f . p) - s), ((f . p) + s).[ c= (f .: ( Ball (p,e))) by A6, A10;

          take Q = ( R^1 ].((f . p) - s), ((f . p) + s).[);

          thus Q is open;

          (f .: ( Ball (p,e))) c= (f .: A) by A11, A12, RELAT_1: 123;

          hence Q c= (f .: A) by A13;

          thus x in Q by A9, TOPREAL6: 15;

        end;

        thus thesis;

      end;

      hence (f .: A) is open by TOPS_1: 25;

    end;

    theorem :: TOPS_4:14

    for f be Function of R^1 , ( TOP-REAL m) holds f is open iff for p be Point of R^1 , r be positive Real holds ex s be positive Real st ( Ball ((f . p),s)) c= (f .: ].(p - r), (p + r).[)

    proof

      let f be Function of R^1 , ( TOP-REAL m);

      

       A1: the TopStruct of ( TOP-REAL m) = ( TopSpaceMetr ( Euclid m)) by EUCLID:def 8;

      then

      reconsider f1 = f as Function of R^1 , ( TopSpaceMetr ( Euclid m));

      thus f is open implies for p be Point of R^1 , r be positive Real holds ex s be positive Real st ( Ball ((f . p),s)) c= (f .: ].(p - r), (p + r).[)

      proof

        assume

         A2: f is open;

        let p be Point of R^1 , r be positive Real;

        reconsider p1 = p as Point of RealSpace ;

        reconsider q1 = (f . p) as Point of ( Euclid m) by EUCLID: 67;

        f1 is open by A1, A2, Th1;

        then

        consider s be positive Real such that

         A3: ( Ball (q1,s)) c= (f1 .: ( Ball (p1,r))) by Th6;

         ].(p - r), (p + r).[ = ( Ball (p1,r)) & ( Ball ((f . p),s)) = ( Ball (q1,s)) by FRECHET: 7, TOPREAL9: 13;

        hence thesis by A3;

      end;

      assume

       A4: for p be Point of R^1 , r be positive Real holds ex s be positive Real st ( Ball ((f . p),s)) c= (f .: ].(p - r), (p + r).[);

      for p be Point of RealSpace , q be Point of ( Euclid m), r be positive Real st q = (f1 . p) holds ex s be positive Real st ( Ball (q,s)) c= (f1 .: ( Ball (p,r)))

      proof

        let p be Point of RealSpace , q be Point of ( Euclid m), r be positive Real such that

         A5: q = (f1 . p);

        reconsider p1 = p as Point of R^1 ;

        consider s be positive Real such that

         A6: ( Ball ((f . p1),s)) c= (f .: ].(p1 - r), (p1 + r).[) by A4;

         ].(p1 - r), (p1 + r).[ = ( Ball (p,r)) & ( Ball ((f . p1),s)) = ( Ball (q,s)) by A5, FRECHET: 7, TOPREAL9: 13;

        hence thesis by A6;

      end;

      then f1 is open by Th6;

      hence thesis by A1, Th1;

    end;

    begin

    theorem :: TOPS_4:15

    for f be Function of T, ( TopSpaceMetr M) holds f is continuous iff for p be Point of T, q be Point of M, r be positive Real st q = (f . p) holds ex W be open Subset of T st p in W & (f .: W) c= ( Ball (q,r))

    proof

      let f be Function of T, ( TopSpaceMetr M);

      thus f is continuous implies for p be Point of T, q be Point of M, r be positive Real st q = (f . p) holds ex W be open Subset of T st p in W & (f .: W) c= ( Ball (q,r))

      proof

        assume

         A1: f is continuous;

        let p be Point of T;

        let q be Point of M;

        let r be positive Real;

        assume

         A2: (f . p) = q;

        reconsider V = ( Ball (q,r)) as Subset of ( TopSpaceMetr M);

        

         A3: q in ( Ball (q,r)) by GOBOARD6: 1;

        V is open by TOPMETR: 14;

        then ex W be Subset of T st p in W & W is open & (f .: W) c= V by A1, A2, A3, JGRAPH_2: 10;

        hence thesis;

      end;

      assume

       A4: for p be Point of T, q be Point of M, r be positive Real st q = (f . p) holds ex W be open Subset of T st p in W & (f .: W) c= ( Ball (q,r));

      for p be Point of T, V be Subset of ( TopSpaceMetr M) st (f . p) in V & V is open holds ex W be Subset of T st p in W & W is open & (f .: W) c= V

      proof

        let p be Point of T, V be Subset of ( TopSpaceMetr M) such that

         A5: (f . p) in V;

        reconsider u = (f . p) as Point of M;

        assume V is open;

        then ( Int V) = V by TOPS_1: 23;

        then

        consider e be Real such that

         A6: e > 0 & ( Ball (u,e)) c= V by A5, GOBOARD6: 4;

        ex W be open Subset of T st p in W & (f .: W) c= ( Ball (u,e)) by A4, A6;

        hence thesis by A6, XBOOLE_1: 1;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPS_4:16

    for f be Function of ( TopSpaceMetr M), T holds f is continuous iff for p be Point of M, V be open Subset of T st (f . p) in V holds ex s be positive Real st (f .: ( Ball (p,s))) c= V

    proof

      let f be Function of ( TopSpaceMetr M), T;

      hereby

        assume

         A1: f is continuous;

        let p be Point of M;

        let V be open Subset of T;

        assume (f . p) in V;

        then

        consider W be Subset of ( TopSpaceMetr M) such that

         A2: p in W and

         A3: W is open and

         A4: (f .: W) c= V by A1, JGRAPH_2: 10;

        ( Int W) = W by A3, TOPS_1: 23;

        then

        consider s be Real such that

         A5: s > 0 and

         A6: ( Ball (p,s)) c= W by A2, GOBOARD6: 4;

        reconsider s as positive Real by A5;

        take s;

        (f .: ( Ball (p,s))) c= (f .: W) by A6, RELAT_1: 123;

        hence (f .: ( Ball (p,s))) c= V by A4;

      end;

      assume

       A7: for p be Point of M, V be open Subset of T st (f . p) in V holds ex s be positive Real st (f .: ( Ball (p,s))) c= V;

      for p be Point of ( TopSpaceMetr M), V be Subset of T st (f . p) in V & V is open holds ex W be Subset of ( TopSpaceMetr M) st p in W & W is open & (f .: W) c= V

      proof

        let p be Point of ( TopSpaceMetr M), V be Subset of T such that

         A8: (f . p) in V and

         A9: V is open;

        reconsider u = p as Point of M;

        consider s be positive Real such that

         A10: (f .: ( Ball (u,s))) c= V by A7, A8, A9;

        reconsider W = ( Ball (u,s)) as Subset of ( TopSpaceMetr M);

        take W;

        thus p in W by GOBOARD6: 1;

        thus W is open by TOPMETR: 14;

        thus thesis by A10;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPS_4:17

    

     Th17: for f be Function of ( TopSpaceMetr M1), ( TopSpaceMetr M2) holds f is continuous iff for p be Point of M1, q be Point of M2, r be positive Real st q = (f . p) holds ex s be positive Real st (f .: ( Ball (p,s))) c= ( Ball (q,r))

    proof

      let f be Function of ( TopSpaceMetr M1), ( TopSpaceMetr M2);

      hereby

        assume

         A1: f is continuous;

        let p be Point of M1;

        let q be Point of M2;

        let r be positive Real;

        assume that

         A2: q = (f . p);

        consider s be Real such that

         A3: s > 0 and

         A4: for w be Element of M1, w1 be Element of M2 st w1 = (f . w) & ( dist (p,w)) < s holds ( dist (q,w1)) < r by A1, A2, UNIFORM1: 4;

        reconsider s as positive Real by A3;

        take s;

        thus (f .: ( Ball (p,s))) c= ( Ball (q,r))

        proof

          let y be object;

          assume y in (f .: ( Ball (p,s)));

          then

          consider x be Point of ( TopSpaceMetr M1) such that

           A5: x in ( Ball (p,s)) and

           A6: (f . x) = y by FUNCT_2: 65;

          reconsider x1 = x as Point of M1;

          reconsider y1 = y as Point of M2 by A6;

          ( dist (p,x1)) < s by A5, METRIC_1: 11;

          then ( dist (q,y1)) < r by A6, A4;

          hence y in ( Ball (q,r)) by METRIC_1: 11;

        end;

      end;

      assume

       A7: for p be Point of M1, q be Point of M2, r be positive Real st q = (f . p) holds ex s be positive Real st (f .: ( Ball (p,s))) c= ( Ball (q,r));

      for r be Real, u be Element of M1, u1 be Element of M2 st r > 0 & u1 = (f . u) holds ex s be Real st s > 0 & for w be Element of M1, w1 be Element of M2 st w1 = (f . w) & ( dist (u,w)) < s holds ( dist (u1,w1)) < r

      proof

        let r be Real, u be Element of M1, u1 be Element of M2;

        assume r > 0 & u1 = (f . u);

        then

        consider s be positive Real such that

         A8: (f .: ( Ball (u,s))) c= ( Ball (u1,r)) by A7;

        take s;

        thus s > 0 ;

        let w be Element of M1, w1 be Element of M2 such that

         A9: w1 = (f . w);

        assume ( dist (u,w)) < s;

        then w in ( Ball (u,s)) by METRIC_1: 11;

        then (f . w) in (f .: ( Ball (u,s))) by FUNCT_2: 35;

        hence thesis by A8, A9, METRIC_1: 11;

      end;

      hence thesis by UNIFORM1: 3;

    end;

    theorem :: TOPS_4:18

    for f be Function of T, ( TOP-REAL m) holds f is continuous iff for p be Point of T, r be positive Real holds ex W be open Subset of T st p in W & (f .: W) c= ( Ball ((f . p),r))

    proof

      let f be Function of T, ( TOP-REAL m);

      

       A1: m in NAT by ORDINAL1:def 12;

      thus f is continuous implies for p be Point of T, r be positive Real holds ex W be open Subset of T st p in W & (f .: W) c= ( Ball ((f . p),r))

      proof

        assume

         A2: f is continuous;

        let p be Point of T;

        let r be positive Real;

        (f . p) in ( Ball ((f . p),r)) by A1, TOPGEN_5: 13;

        then ex W be Subset of T st p in W & W is open & (f .: W) c= ( Ball ((f . p),r)) by A2, JGRAPH_2: 10;

        hence thesis;

      end;

      assume

       A3: for p be Point of T, r be positive Real holds ex W be open Subset of T st p in W & (f .: W) c= ( Ball ((f . p),r));

      for p be Point of T, V be Subset of ( TOP-REAL m) st (f . p) in V & V is open holds ex W be Subset of T st p in W & W is open & (f .: W) c= V

      proof

        let p be Point of T, V be Subset of ( TOP-REAL m) such that

         A4: (f . p) in V;

        reconsider u = (f . p) as Point of ( Euclid m) by EUCLID: 67;

        assume V is open;

        then ( Int V) = V by TOPS_1: 23;

        then

        consider e be Real such that

         A5: e > 0 and

         A6: ( Ball (u,e)) c= V by A4, GOBOARD6: 5;

        

         A7: ( Ball (u,e)) = ( Ball ((f . p),e)) by TOPREAL9: 13;

        ex W be open Subset of T st p in W & (f .: W) c= ( Ball ((f . p),e)) by A3, A5;

        hence thesis by A6, A7, XBOOLE_1: 1;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPS_4:19

    for f be Function of ( TOP-REAL m), T holds f is continuous iff for p be Point of ( TOP-REAL m), V be open Subset of T st (f . p) in V holds ex s be positive Real st (f .: ( Ball (p,s))) c= V

    proof

      let f be Function of ( TOP-REAL m), T;

      

       A1: m in NAT by ORDINAL1:def 12;

      hereby

        assume

         A2: f is continuous;

        let p be Point of ( TOP-REAL m);

        let V be open Subset of T;

        assume (f . p) in V;

        then

        consider W be Subset of ( TOP-REAL m) such that

         A3: p in W and

         A4: W is open and

         A5: (f .: W) c= V by A2, JGRAPH_2: 10;

        reconsider u = p as Point of ( Euclid m) by EUCLID: 67;

        ( Int W) = W by A4, TOPS_1: 23;

        then

        consider s be Real such that

         A6: s > 0 and

         A7: ( Ball (u,s)) c= W by A3, GOBOARD6: 5;

        reconsider s as positive Real by A6;

        take s;

        ( Ball (u,s)) = ( Ball (p,s)) by TOPREAL9: 13;

        then (f .: ( Ball (p,s))) c= (f .: W) by A7, RELAT_1: 123;

        hence (f .: ( Ball (p,s))) c= V by A5;

      end;

      assume

       A8: for p be Point of ( TOP-REAL m), V be open Subset of T st (f . p) in V holds ex s be positive Real st (f .: ( Ball (p,s))) c= V;

      for p be Point of ( TOP-REAL m), V be Subset of T st (f . p) in V & V is open holds ex W be Subset of ( TOP-REAL m) st p in W & W is open & (f .: W) c= V

      proof

        let p be Point of ( TOP-REAL m), V be Subset of T such that

         A9: (f . p) in V and

         A10: V is open;

        consider s be positive Real such that

         A11: (f .: ( Ball (p,s))) c= V by A8, A9, A10;

        take W = ( Ball (p,s));

        thus p in W by A1, TOPGEN_5: 13;

        thus W is open;

        thus thesis by A11;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPS_4:20

    for f be Function of ( TOP-REAL m), ( TOP-REAL n) holds f is continuous iff for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st (f .: ( Ball (p,s))) c= ( Ball ((f . p),r))

    proof

      let f be Function of ( TOP-REAL m), ( TOP-REAL n);

      

       A1: the TopStruct of ( TOP-REAL m) = ( TopSpaceMetr ( Euclid m)) & the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      then

      reconsider f1 = f as Function of ( TopSpaceMetr ( Euclid m)), ( TopSpaceMetr ( Euclid n));

      hereby

        assume

         A2: f is continuous;

        let p be Point of ( TOP-REAL m);

        let r be positive Real;

        reconsider p1 = p as Point of ( Euclid m) by EUCLID: 67;

        reconsider q1 = (f . p) as Point of ( Euclid n) by EUCLID: 67;

        f1 is continuous by A1, A2, YELLOW12: 36;

        then

        consider s be positive Real such that

         A3: (f1 .: ( Ball (p1,s))) c= ( Ball (q1,r)) by Th17;

        take s;

        ( Ball (p1,s)) = ( Ball (p,s)) & ( Ball (q1,r)) = ( Ball ((f . p),r)) by TOPREAL9: 13;

        hence (f .: ( Ball (p,s))) c= ( Ball ((f . p),r)) by A3;

      end;

      assume

       A4: for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st (f .: ( Ball (p,s))) c= ( Ball ((f . p),r));

      for p be Point of ( Euclid m), q be Point of ( Euclid n), r be positive Real st q = (f1 . p) holds ex s be positive Real st (f1 .: ( Ball (p,s))) c= ( Ball (q,r))

      proof

        let p be Point of ( Euclid m), q be Point of ( Euclid n), r be positive Real such that

         A5: q = (f1 . p);

        reconsider p1 = p as Point of ( TOP-REAL m) by EUCLID: 67;

        consider s be positive Real such that

         A6: (f .: ( Ball (p1,s))) c= ( Ball ((f . p1),r)) by A4;

        take s;

        ( Ball (p1,s)) = ( Ball (p,s)) & ( Ball ((f . p1),r)) = ( Ball (q,r)) by A5, TOPREAL9: 13;

        hence thesis by A6;

      end;

      then f1 is continuous by Th17;

      hence thesis by A1, YELLOW12: 36;

    end;

    theorem :: TOPS_4:21

    for f be Function of T, R^1 holds f is continuous iff for p be Point of T, r be positive Real holds ex W be open Subset of T st p in W & (f .: W) c= ].((f . p) - r), ((f . p) + r).[

    proof

      let f be Function of T, R^1 ;

      thus f is continuous implies for p be Point of T, r be positive Real holds ex W be open Subset of T st p in W & (f .: W) c= ].((f . p) - r), ((f . p) + r).[

      proof

        assume

         A1: f is continuous;

        let p be Point of T;

        let r be positive Real;

        

         A2: (f . p) in ].((f . p) - r), ((f . p) + r).[ by TOPREAL6: 15;

        ( R^1 ].((f . p) - r), ((f . p) + r).[) is open;

        then ex W be Subset of T st p in W & W is open & (f .: W) c= ].((f . p) - r), ((f . p) + r).[ by A1, A2, JGRAPH_2: 10;

        hence thesis;

      end;

      assume

       A3: for p be Point of T, r be positive Real holds ex W be open Subset of T st p in W & (f .: W) c= ].((f . p) - r), ((f . p) + r).[;

      for p be Point of T, V be Subset of R^1 st (f . p) in V & V is open holds ex W be Subset of T st p in W & W is open & (f .: W) c= V

      proof

        let p be Point of T, V be Subset of R^1 such that

         A4: (f . p) in V;

        assume V is open;

        then

        consider r be Real such that

         A5: r > 0 and

         A6: ].((f . p) - r), ((f . p) + r).[ c= V by A4, FRECHET: 8;

        ex W be open Subset of T st p in W & (f .: W) c= ].((f . p) - r), ((f . p) + r).[ by A3, A5;

        hence thesis by A6, XBOOLE_1: 1;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPS_4:22

    for f be Function of R^1 , T holds f is continuous iff for p be Point of R^1 , V be open Subset of T st (f . p) in V holds ex s be positive Real st (f .: ].(p - s), (p + s).[) c= V

    proof

      let f be Function of R^1 , T;

      hereby

        assume

         A1: f is continuous;

        let p be Point of R^1 ;

        let V be open Subset of T;

        assume (f . p) in V;

        then

        consider W be Subset of R^1 such that

         A2: p in W and

         A3: W is open and

         A4: (f .: W) c= V by A1, JGRAPH_2: 10;

        consider s be Real such that

         A5: s > 0 and

         A6: ].(p - s), (p + s).[ c= W by A2, A3, FRECHET: 8;

        reconsider s as positive Real by A5;

        take s;

        (f .: ].(p - s), (p + s).[) c= (f .: W) by A6, RELAT_1: 123;

        hence (f .: ].(p - s), (p + s).[) c= V by A4;

      end;

      assume

       A7: for p be Point of R^1 , V be open Subset of T st (f . p) in V holds ex s be positive Real st (f .: ].(p - s), (p + s).[) c= V;

      for p be Point of R^1 , V be Subset of T st (f . p) in V & V is open holds ex W be Subset of R^1 st p in W & W is open & (f .: W) c= V

      proof

        let p be Point of R^1 , V be Subset of T such that

         A8: (f . p) in V and

         A9: V is open;

        consider s be positive Real such that

         A10: (f .: ].(p - s), (p + s).[) c= V by A7, A8, A9;

        take W = ( R^1 ].(p - s), (p + s).[);

        thus p in W by TOPREAL6: 15;

        thus W is open;

        thus thesis by A10;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPS_4:23

    for f be Function of R^1 , R^1 holds f is continuous iff for p be Point of R^1 , r be positive Real holds ex s be positive Real st (f .: ].(p - s), (p + s).[) c= ].((f . p) - r), ((f . p) + r).[

    proof

      let f be Function of R^1 , R^1 ;

      hereby

        assume

         A1: f is continuous;

        let p be Point of R^1 ;

        let r be positive Real;

        reconsider p1 = p, q1 = (f . p) as Point of RealSpace ;

        consider s be positive Real such that

         A2: (f .: ( Ball (p1,s))) c= ( Ball (q1,r)) by A1, Th17;

        take s;

        ( Ball (p1,s)) = ].(p1 - s), (p1 + s).[ & ( Ball (q1,r)) = ].(q1 - r), (q1 + r).[ by FRECHET: 7;

        hence (f .: ].(p - s), (p + s).[) c= ].((f . p) - r), ((f . p) + r).[ by A2;

      end;

      assume

       A3: for p be Point of R^1 , r be positive Real holds ex s be positive Real st (f .: ].(p - s), (p + s).[) c= ].((f . p) - r), ((f . p) + r).[;

      for p,q be Point of RealSpace , r be positive Real st q = (f . p) holds ex s be positive Real st (f .: ( Ball (p,s))) c= ( Ball (q,r))

      proof

        let p,q be Point of RealSpace , r be positive Real such that

         A4: q = (f . p);

        consider s be positive Real such that

         A5: (f .: ].(p - s), (p + s).[) c= ].((f . p) - r), ((f . p) + r).[ by A3;

        take s;

        ( Ball (p,s)) = ].(p - s), (p + s).[ & ( Ball (q,r)) = ].(q - r), (q + r).[ by FRECHET: 7;

        hence thesis by A5, A4;

      end;

      hence f is continuous by Th17;

    end;

    theorem :: TOPS_4:24

    for f be Function of ( TOP-REAL m), R^1 holds f is continuous iff for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st (f .: ( Ball (p,s))) c= ].((f . p) - r), ((f . p) + r).[

    proof

      let f be Function of ( TOP-REAL m), R^1 ;

      

       A1: the TopStruct of ( TOP-REAL m) = ( TopSpaceMetr ( Euclid m)) by EUCLID:def 8;

      then

      reconsider f1 = f as Function of ( TopSpaceMetr ( Euclid m)), R^1 ;

      hereby

        assume

         A2: f is continuous;

        let p be Point of ( TOP-REAL m);

        let r be positive Real;

        reconsider p1 = p as Point of ( Euclid m) by EUCLID: 67;

        reconsider q1 = (f . p) as Point of RealSpace ;

        f1 is continuous by A1, A2, YELLOW12: 36;

        then

        consider s be positive Real such that

         A3: (f .: ( Ball (p1,s))) c= ( Ball (q1,r)) by A1, Th17;

        take s;

        ( Ball (p1,s)) = ( Ball (p,s)) & ( Ball (q1,r)) = ].((f . p) - r), ((f . p) + r).[ by FRECHET: 7, TOPREAL9: 13;

        hence (f .: ( Ball (p,s))) c= ].((f . p) - r), ((f . p) + r).[ by A3;

      end;

      assume

       A4: for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st (f .: ( Ball (p,s))) c= ].((f . p) - r), ((f . p) + r).[;

      for p be Point of ( Euclid m), q be Point of RealSpace , r be positive Real st q = (f1 . p) holds ex s be positive Real st (f1 .: ( Ball (p,s))) c= ( Ball (q,r))

      proof

        let p be Point of ( Euclid m), q be Point of RealSpace , r be positive Real such that

         A5: q = (f1 . p);

        reconsider p1 = p as Point of ( TOP-REAL m) by EUCLID: 67;

        consider s be positive Real such that

         A6: (f .: ( Ball (p1,s))) c= ].((f . p) - r), ((f . p) + r).[ by A4;

        take s;

        ( Ball (p1,s)) = ( Ball (p,s)) & ].((f . p) - r), ((f . p) + r).[ = ( Ball (q,r)) by A5, FRECHET: 7, TOPREAL9: 13;

        hence thesis by A6;

      end;

      then f1 is continuous by Th17;

      hence thesis by A1, YELLOW12: 36;

    end;

    theorem :: TOPS_4:25

    for f be Function of R^1 , ( TOP-REAL m) holds f is continuous iff for p be Point of R^1 , r be positive Real holds ex s be positive Real st (f .: ].(p - s), (p + s).[) c= ( Ball ((f . p),r))

    proof

      let f be Function of R^1 , ( TOP-REAL m);

      

       A1: the TopStruct of ( TOP-REAL m) = ( TopSpaceMetr ( Euclid m)) by EUCLID:def 8;

      then

      reconsider f1 = f as Function of R^1 , ( TopSpaceMetr ( Euclid m));

      hereby

        assume

         A2: f is continuous;

        let p be Point of R^1 ;

        let r be positive Real;

        reconsider p1 = p as Point of RealSpace ;

        reconsider q1 = (f . p) as Point of ( Euclid m) by EUCLID: 67;

        f1 is continuous by A1, A2, YELLOW12: 36;

        then

        consider s be positive Real such that

         A3: (f1 .: ( Ball (p1,s))) c= ( Ball (q1,r)) by Th17;

        take s;

        ( Ball (p1,s)) = ].(p - s), (p + s).[ & ( Ball (q1,r)) = ( Ball ((f . p),r)) by FRECHET: 7, TOPREAL9: 13;

        hence (f .: ].(p - s), (p + s).[) c= ( Ball ((f . p),r)) by A3;

      end;

      assume

       A4: for p be Point of R^1 , r be positive Real holds ex s be positive Real st (f .: ].(p - s), (p + s).[) c= ( Ball ((f . p),r));

      for p be Point of RealSpace , q be Point of ( Euclid m), r be positive Real st q = (f . p) holds ex s be positive Real st (f .: ( Ball (p,s))) c= ( Ball (q,r))

      proof

        let p be Point of RealSpace , q be Point of ( Euclid m), r be positive Real such that

         A5: q = (f . p);

        reconsider p1 = p as Point of R^1 ;

        consider s be positive Real such that

         A6: (f .: ].(p - s), (p + s).[) c= ( Ball ((f . p1),r)) by A4;

        take s;

         ].(p - s), (p + s).[ = ( Ball (p,s)) & ( Ball ((f . p1),r)) = ( Ball (q,r)) by A5, FRECHET: 7, TOPREAL9: 13;

        hence thesis by A6;

      end;

      then f1 is continuous by A1, Th17;

      hence thesis by A1, YELLOW12: 36;

    end;