lopban_6.miz



    begin

    theorem :: LOPBAN_6:1

    

     Th1: for x,y be Real st 0 <= x & x < y holds ex s0 be Real st 0 < s0 & x < (y / (1 + s0)) & (y / (1 + s0)) < y

    proof

      let x,y be Real;

      assume that

       A1: 0 <= x and

       A2: x < y;

      ex s0 be Real st 0 < s0 & x < (y / (1 + s0)) & (y / (1 + s0)) < y

      proof

        consider s be Real such that

         A3: x < s and

         A4: s < y by A2, XREAL_1: 5;

        now

          per cases by A1;

            case

             A5: 0 = x;

            set s0 = s;

            y < (y * (1 + s0)) by A1, A3, A4, XREAL_1: 29, XREAL_1: 155;

            hence 0 < s0 & x < (y / (1 + s0)) & (y / (1 + s0)) < y by A3, A4, A5, XREAL_1: 83, XREAL_1: 139;

          end;

            case

             A6: 0 < x;

            set s0 = ((s / x) - 1);

            

             A7: ((1 + s0) " ) = (1 / (1 + s0)) by XCMPLX_1: 215;

            then

             A8: (s * ((1 + s0) " )) = ((s * 1) / (1 + s0)) by XCMPLX_1: 74;

            ((1 + s0) * x) = ((x / x) * s) by XCMPLX_1: 75;

            then ((1 + s0) * x) = (1 * s) by A6, XCMPLX_1: 60;

            then

             A9: ((((1 + s0) " ) * (1 + s0)) * x) = (s * ((1 + s0) " ));

             0 < (1 + s0) by A3, A6, XREAL_1: 187;

            then

             A10: (((1 + s0) " ) * (1 + s0)) = 1 by A7, XCMPLX_1: 106;

            

             A11: 1 < (1 + s0) by A3, A6, XREAL_1: 187;

            then y < (y * (1 + s0)) by A1, A2, XREAL_1: 155;

            hence 0 < s0 & x < (y / (1 + s0)) & (y / (1 + s0)) < y by A4, A11, A9, A10, A8, XREAL_1: 50, XREAL_1: 74, XREAL_1: 83;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    scheme :: LOPBAN_6:sch1

    RecExD3 { D() -> non empty set , A() -> Element of D() , B() -> Element of D() , P[ object, object, object, object] } :

ex f be sequence of D() st (f . 0 ) = A() & (f . 1) = B() & for n be Nat holds P[n, (f . n), (f . (n + 1)), (f . (n + 2))]

      provided

       A1: for n be Nat holds for x,y be Element of D() holds ex z be Element of D() st P[n, x, y, z];

      defpred Q[ set, set, set] means P[$1, ($2 `1 ), ($2 `2 ), ($3 `2 )] & ($2 `2 ) = ($3 `1 );

      

       A2: for n be Nat holds for x be Element of [:D(), D():] holds ex y be Element of [:D(), D():] st Q[n, x, y]

      proof

        let n be Nat;

        let x be Element of [:D(), D():];

        set z = (x `1 );

        set w = (x `2 );

        reconsider z, w as Element of D();

        consider s be Element of D() such that

         A3: P[n, z, w, s] by A1;

        set y = [w, s];

        reconsider y as Element of [:D(), D():];

        take y;

        thus thesis by A3;

      end;

      consider g be sequence of [:D(), D():] such that

       A4: (g . 0 ) = [A(), B()] & for n be Nat holds Q[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 2( A2);

      deffunc F( Nat) = ((g . $1) `1 );

      

       A5: for x be Element of NAT holds F(x) in D();

      consider f be sequence of D() such that

       A6: for x be Element of NAT holds (f . x) = F(x) from FUNCT_2:sch 8( A5);

       A7:

      now

        let n be Nat;

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        

         A8: (f . n) = ((g . nn) `1 ) by A6;

         Q[(n + 1), (g . (n + 1)), (g . ((n + 1) + 1))] by A4;

        then

         A9: (f . (n + 2)) = ((g . (n + 1)) `2 ) by A6;

        (f . (n + 1)) = ((g . (n + 1)) `1 ) by A6

        .= ((g . nn) `2 ) by A4;

        hence P[n, (f . n), (f . (n + 1)), (f . (n + 2))] by A4, A8, A9;

      end;

      take f;

      

       A10: Q[ 0 , (g . 0 ), (g . ( 0 + 1))] by A4;

      

       A11: (f . 0 ) = ((g . 0 ) `1 ) by A6

      .= A() by A4;

      (f . 1) = ((g . 1) `1 ) by A6

      .= B() by A4, A10;

      hence thesis by A11, A7;

    end;

    reserve X,Y for RealNormSpace;

    theorem :: LOPBAN_6:2

    

     Th2: for y1 be Point of X, r be Real holds ( Ball (y1,r)) = (y1 + ( Ball (( 0. X),r)))

    proof

      let y1 be Point of X, r be Real;

      thus ( Ball (y1,r)) c= (y1 + ( Ball (( 0. X),r)))

      proof

        let t be object;

        assume

         A1: t in ( Ball (y1,r));

        then

        reconsider z1 = t as Point of X;

        set z0 = (z1 - y1);

        ex zz1 be Point of X st z1 = zz1 & ||.(y1 - zz1).|| < r by A1;

        then ||.( - z0).|| < r by RLVECT_1: 33;

        then ||.(( 0. X) - z0).|| < r by RLVECT_1: 14;

        then

         A2: z0 in ( Ball (( 0. X),r));

        (z0 + y1) = (z1 + (( - y1) + y1)) by RLVECT_1:def 3;

        then (z0 + y1) = (z1 + ( 0. X)) by RLVECT_1: 5;

        then z1 = (z0 + y1) by RLVECT_1: 4;

        hence thesis by A2;

      end;

      let t be object;

      assume t in (y1 + ( Ball (( 0. X),r)));

      then

      consider z0 be Point of X such that

       A3: t = (y1 + z0) and

       A4: z0 in ( Ball (( 0. X),r));

      set z1 = (z0 + y1);

      ex zz0 be Point of X st z0 = zz0 & ||.(( 0. X) - zz0).|| < r by A4;

      then ||.( - z0).|| < r by RLVECT_1: 14;

      then ||.z0.|| < r by NORMSP_1: 2;

      then ||.(z0 + ( 0. X)).|| < r by RLVECT_1: 4;

      then ||.(z0 + (y1 + ( - y1))).|| < r by RLVECT_1: 5;

      then ||.(z1 - y1).|| < r by RLVECT_1:def 3;

      then ||.(y1 - z1).|| < r by NORMSP_1: 7;

      hence thesis by A3;

    end;

    theorem :: LOPBAN_6:3

    

     Th3: for r,a be Real st 0 < a holds ( Ball (( 0. X),(a * r))) = (a * ( Ball (( 0. X),r)))

    proof

      let r,a be Real;

      assume

       A1: 0 < a;

      thus ( Ball (( 0. X),(a * r))) c= (a * ( Ball (( 0. X),r)))

      proof

        let z be object;

        assume

         A2: z in ( Ball (( 0. X),(a * r)));

        then

        reconsider z1 = z as Point of X;

        ex zz1 be Point of X st z1 = zz1 & ||.(( 0. X) - zz1).|| < (a * r) by A2;

        then ||.( - z1).|| < (a * r) by RLVECT_1: 14;

        then ||.z1.|| < (a * r) by NORMSP_1: 2;

        then ((a " ) * ||.z1.||) < ((a " ) * (a * r)) by A1, XREAL_1: 68;

        then ((a " ) * ||.z1.||) < ((a * (a " )) * r);

        then

         A3: ((a " ) * ||.z1.||) < (1 * r) by A1, XCMPLX_0:def 7;

        set y1 = ((a " ) * z1);

         ||.y1.|| = ( |.(a " ).| * ||.z1.||) by NORMSP_1:def 1

        .= ((a " ) * ||.z1.||) by A1, ABSVALUE:def 1;

        then ||.( - y1).|| < r by A3, NORMSP_1: 2;

        then ||.(( 0. X) - y1).|| < r by RLVECT_1: 14;

        then

         A4: y1 in ( Ball (( 0. X),r));

        (a * y1) = ((a * (a " )) * z1) by RLVECT_1:def 7

        .= (1 * z1) by A1, XCMPLX_0:def 7

        .= z1 by RLVECT_1:def 8;

        hence thesis by A4;

      end;

      let z be object;

      assume

       A5: z in (a * ( Ball (( 0. X),r)));

      then

      reconsider z1 = z as Point of X;

      consider y1 be Point of X such that

       A6: z1 = (a * y1) and

       A7: y1 in ( Ball (( 0. X),r)) by A5;

      ex yy1 be Point of X st y1 = yy1 & ||.(( 0. X) - yy1).|| < r by A7;

      then ||.( - y1).|| < r by RLVECT_1: 14;

      then

       A8: ||.y1.|| < r by NORMSP_1: 2;

       ||.z1.|| = ( |.a.| * ||.y1.||) by A6, NORMSP_1:def 1

      .= (a * ||.y1.||) by A1, ABSVALUE:def 1;

      then ||.z1.|| < (a * r) by A1, A8, XREAL_1: 68;

      then ||.( - z1).|| < (a * r) by NORMSP_1: 2;

      then ||.(( 0. X) - z1).|| < (a * r) by RLVECT_1: 14;

      hence thesis;

    end;

    theorem :: LOPBAN_6:4

    for T be LinearOperator of X, Y, B0,B1 be Subset of X holds (T .: (B0 + B1)) = ((T .: B0) + (T .: B1))

    proof

      let T be LinearOperator of X, Y, B0,B1 be Subset of X;

      thus (T .: (B0 + B1)) c= ((T .: B0) + (T .: B1))

      proof

        let t be object;

        assume t in (T .: (B0 + B1));

        then

        consider z1 be object such that z1 in the carrier of X and

         A1: z1 in (B0 + B1) and

         A2: t = (T . z1) by FUNCT_2: 64;

        consider x1,x2 be Element of X such that

         A3: z1 = (x1 + x2) and

         A4: x1 in B0 & x2 in B1 by A1;

        

         A5: (T . x1) in (T .: B0) & (T . x2) in (T .: B1) by A4, FUNCT_2: 35;

        t = ((T . x1) + (T . x2)) by A2, A3, VECTSP_1:def 20;

        hence thesis by A5;

      end;

      let t be object;

      assume t in ((T .: B0) + (T .: B1));

      then

      consider tz0,tz1 be Point of Y such that

       A6: t = (tz0 + tz1) and

       A7: tz0 in (T .: B0) and

       A8: tz1 in (T .: B1);

      consider z1 be Element of X such that

       A9: z1 in B1 and

       A10: tz1 = (T . z1) by A8, FUNCT_2: 65;

      consider z0 be Element of X such that

       A11: z0 in B0 and

       A12: tz0 = (T . z0) by A7, FUNCT_2: 65;

      reconsider z1 as Point of X;

      reconsider z0 as Point of X;

      

       A13: (z0 + z1) in (B0 + B1) by A11, A9;

      t = (T . (z0 + z1)) by A6, A12, A10, VECTSP_1:def 20;

      hence thesis by A13, FUNCT_2: 35;

    end;

    theorem :: LOPBAN_6:5

    

     Th5: for T be LinearOperator of X, Y, B0 be Subset of X, a be Real holds (T .: (a * B0)) = (a * (T .: B0))

    proof

      let T be LinearOperator of X, Y, B0 be Subset of X, a be Real;

      thus (T .: (a * B0)) c= (a * (T .: B0))

      proof

        let t be object;

        assume t in (T .: (a * B0));

        then

        consider z1 be object such that z1 in the carrier of X and

         A1: z1 in (a * B0) and

         A2: t = (T . z1) by FUNCT_2: 64;

        consider x1 be Element of X such that

         A3: z1 = (a * x1) and

         A4: x1 in B0 by A1;

        

         A5: (T . x1) in (T .: B0) by A4, FUNCT_2: 35;

        t = (a * (T . x1)) by A2, A3, LOPBAN_1:def 5;

        hence thesis by A5;

      end;

      let t be object;

      assume t in (a * (T .: B0));

      then

      consider tz0 be Point of Y such that

       A6: t = (a * tz0) and

       A7: tz0 in (T .: B0);

      consider z0 be Element of X such that

       A8: z0 in B0 and

       A9: tz0 = (T . z0) by A7, FUNCT_2: 65;

      reconsider z0 as Point of X;

      set z1 = (a * z0);

      

       A10: z1 in (a * B0) by A8;

      t = (T . z1) by A6, A9, LOPBAN_1:def 5;

      hence thesis by A10, FUNCT_2: 35;

    end;

    theorem :: LOPBAN_6:6

    

     Th6: for T be LinearOperator of X, Y, B0 be Subset of X, x1 be Point of X holds (T .: (x1 + B0)) = ((T . x1) + (T .: B0))

    proof

      let T be LinearOperator of X, Y, B0 be Subset of X, x1 be Point of X;

      thus (T .: (x1 + B0)) c= ((T . x1) + (T .: B0))

      proof

        let t be object;

        assume t in (T .: (x1 + B0));

        then

        consider z1 be object such that

         A1: z1 in the carrier of X and

         A2: z1 in (x1 + B0) and

         A3: t = (T . z1) by FUNCT_2: 64;

        reconsider z1 as Point of X by A1;

        consider z0 be Element of X such that

         A4: z1 = (x1 + z0) and

         A5: z0 in B0 by A2;

        

         A6: (T . z0) in (T .: B0) by A5, FUNCT_2: 35;

        t = ((T . x1) + (T . z0)) by A3, A4, VECTSP_1:def 20;

        hence thesis by A6;

      end;

      let t be object;

      assume t in ((T . x1) + (T .: B0));

      then

      consider tz0 be Point of Y such that

       A7: t = ((T . x1) + tz0) and

       A8: tz0 in (T .: B0);

      consider z0 be Element of X such that

       A9: z0 in B0 and

       A10: tz0 = (T . z0) by A8, FUNCT_2: 65;

      

       A11: (x1 + z0) in (x1 + B0) by A9;

      t = (T . (x1 + z0)) by A7, A10, VECTSP_1:def 20;

      hence thesis by A11, FUNCT_2: 35;

    end;

    theorem :: LOPBAN_6:7

    for V,W be Subset of X, V1,W1 be Subset of ( LinearTopSpaceNorm X) st V = V1 & W = W1 holds (V + W) = (V1 + W1)

    proof

      let V,W be Subset of X, V1,W1 be Subset of ( LinearTopSpaceNorm X) such that

       A1: V = V1 and

       A2: W = W1;

      thus (V + W) c= (V1 + W1)

      proof

        let x be object;

        assume x in (V + W);

        then

        consider u,v be Point of X such that

         A3: x = (u + v) and

         A4: u in V and

         A5: v in W;

        reconsider v1 = v as Point of ( LinearTopSpaceNorm X) by A2, A5;

        reconsider u1 = u as Point of ( LinearTopSpaceNorm X) by A1, A4;

        (u + v) = (u1 + v1) by NORMSP_2:def 4;

        hence thesis by A1, A2, A3, A4, A5;

      end;

      let x be object;

      assume x in (V1 + W1);

      then

      consider u,v be Point of ( LinearTopSpaceNorm X) such that

       A6: x = (u + v) and

       A7: u in V1 and

       A8: v in W1;

      reconsider v1 = v as Point of X by A2, A8;

      reconsider u1 = u as Point of X by A1, A7;

      (u + v) = (u1 + v1) by NORMSP_2:def 4;

      hence thesis by A1, A2, A6, A7, A8;

    end;

    theorem :: LOPBAN_6:8

    

     Th8: for V be Subset of X, x be Point of X, V1 be Subset of ( LinearTopSpaceNorm X), x1 be Point of ( LinearTopSpaceNorm X) st V = V1 & x = x1 holds (x + V) = (x1 + V1)

    proof

      let V be Subset of X, x be Point of X, V1 be Subset of ( LinearTopSpaceNorm X), x1 be Point of ( LinearTopSpaceNorm X) such that

       A1: V = V1 and

       A2: x = x1;

      thus (x + V) c= (x1 + V1)

      proof

        let z be object;

        assume z in (x + V);

        then

        consider u be Point of X such that

         A3: z = (x + u) and

         A4: u in V;

        reconsider u1 = u as Point of ( LinearTopSpaceNorm X) by A1, A4;

        (x + u) = (x1 + u1) by A2, NORMSP_2:def 4;

        hence thesis by A1, A3, A4;

      end;

      let z be object;

      assume z in (x1 + V1);

      then

      consider u1 be Point of ( LinearTopSpaceNorm X) such that

       A5: z = (x1 + u1) and

       A6: u1 in V1;

      reconsider u = u1 as Point of X by A1, A6;

      (x1 + u1) = (x + u) by A2, NORMSP_2:def 4;

      hence thesis by A1, A5, A6;

    end;

    theorem :: LOPBAN_6:9

    

     Th9: for V be Subset of X, a be Real, V1 be Subset of ( LinearTopSpaceNorm X) st V = V1 holds (a * V) = (a * V1)

    proof

      let V be Subset of X, a be Real, V1 be Subset of ( LinearTopSpaceNorm X) such that

       A1: V = V1;

      thus (a * V) c= (a * V1)

      proof

        let z be object;

        assume z in (a * V);

        then

        consider v be Point of X such that

         A2: z = (a * v) and

         A3: v in V;

        reconsider v1 = v as Point of ( LinearTopSpaceNorm X) by A1, A3;

        (a * v) = (a * v1) by NORMSP_2:def 4;

        hence thesis by A1, A2, A3;

      end;

      let z be object;

      assume z in (a * V1);

      then

      consider v be Point of ( LinearTopSpaceNorm X) such that

       A4: z = (a * v) and

       A5: v in V1;

      reconsider v1 = v as Point of X by A1, A5;

      (a * v) = (a * v1) by NORMSP_2:def 4;

      hence thesis by A1, A4, A5;

    end;

    theorem :: LOPBAN_6:10

    

     Th10: for V be Subset of ( TopSpaceNorm X), V1 be Subset of ( LinearTopSpaceNorm X) st V = V1 holds ( Cl V) = ( Cl V1)

    proof

      let V be Subset of ( TopSpaceNorm X), V1 be Subset of ( LinearTopSpaceNorm X) such that

       A1: V = V1;

      thus ( Cl V) c= ( Cl V1)

      proof

        let z be object;

        assume

         A2: z in ( Cl V);

        

         A3: for D1 be Subset of ( LinearTopSpaceNorm X) st D1 is closed holds V1 c= D1 implies z in D1

        proof

          let D1 be Subset of ( LinearTopSpaceNorm X) such that

           A4: D1 is closed;

          reconsider D0 = D1 as Subset of X by NORMSP_2:def 4;

          reconsider D2 = D1 as Subset of ( TopSpaceNorm X) by NORMSP_2:def 4;

          D0 is closed by A4, NORMSP_2: 32;

          then

           A5: D2 is closed by NORMSP_2: 15;

          assume V1 c= D1;

          hence thesis by A1, A2, A5, PRE_TOPC: 15;

        end;

        z in the carrier of X by A2;

        then z in the carrier of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        hence thesis by A3, PRE_TOPC: 15;

      end;

      let z be object;

      assume

       A6: z in ( Cl V1);

      

       A7: for D1 be Subset of ( TopSpaceNorm X) st D1 is closed holds V c= D1 implies z in D1

      proof

        let D1 be Subset of ( TopSpaceNorm X) such that

         A8: D1 is closed;

        reconsider D0 = D1 as Subset of X;

        reconsider D2 = D1 as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        D0 is closed by A8, NORMSP_2: 15;

        then

         A9: D2 is closed by NORMSP_2: 32;

        assume V c= D1;

        hence thesis by A1, A6, A9, PRE_TOPC: 15;

      end;

      z in the carrier of ( LinearTopSpaceNorm X) by A6;

      then z in the carrier of ( TopSpaceNorm X) by NORMSP_2:def 4;

      hence thesis by A7, PRE_TOPC: 15;

    end;

    theorem :: LOPBAN_6:11

    

     Th11: for x be Point of X, r be Real holds ( Ball (( 0. X),r)) = (( - 1) * ( Ball (( 0. X),r)))

    proof

      let x be Point of X, r be Real;

      thus ( Ball (( 0. X),r)) c= (( - 1) * ( Ball (( 0. X),r)))

      proof

        let z be object;

        assume

         A1: z in ( Ball (( 0. X),r));

        then

        reconsider z1 = z as Point of X;

        ex zz1 be Point of X st z1 = zz1 & ||.(( 0. X) - zz1).|| < r by A1;

        then ||.( - z1).|| < r by RLVECT_1: 14;

        then ||.( - ( - z1)).|| < r by NORMSP_1: 2;

        then ||.(( 0. X) - ( - z1)).|| < r by RLVECT_1: 14;

        then

         A2: ( - z1) in ( Ball (( 0. X),r));

        (( - 1) * ( - z1)) = (1 * z1) by RLVECT_1: 26

        .= z1 by RLVECT_1:def 8;

        hence thesis by A2;

      end;

      let z be object;

      assume

       A3: z in (( - 1) * ( Ball (( 0. X),r)));

      then

      reconsider z1 = z as Point of X;

      consider y1 be Point of X such that

       A4: z1 = (( - 1) * y1) and

       A5: y1 in ( Ball (( 0. X),r)) by A3;

      ex zz1 be Point of X st y1 = zz1 & ||.(( 0. X) - zz1).|| < r by A5;

      then ||.( - y1).|| < r by RLVECT_1: 14;

      then ||.( - ( - y1)).|| < r by NORMSP_1: 2;

      then

       A6: ||.(( 0. X) - ( - y1)).|| < r by RLVECT_1: 14;

      ( - y1) = z1 by A4, RLVECT_1: 16;

      hence thesis by A6;

    end;

    theorem :: LOPBAN_6:12

    

     Th12: for x be Point of X, r be Real, V be Subset of ( LinearTopSpaceNorm X) st V = ( Ball (x,r)) holds V is convex

    proof

      let x be Point of X, r be Real, V be Subset of ( LinearTopSpaceNorm X);

      reconsider V1 = ( Ball (x,r)) as Subset of X;

      

       A1: for u,v be Point of X, s be Real st 0 < s & s < 1 & u in V1 & v in V1 holds ((s * u) + ((1 - s) * v)) in V1

      proof

        let u,v be Point of X, s be Real;

        assume that

         A2: 0 < s and

         A3: s < 1 and

         A4: u in V1 and

         A5: v in V1;

        

         A6: ex v1 be Point of X st v = v1 & ||.(x - v1).|| < r by A5;

         0 < |.s.| & ex u1 be Point of X st u = u1 & ||.(x - u1).|| < r by A2, A4, ABSVALUE:def 1;

        then

         A7: ( |.s.| * ||.(x - u).||) < ( |.s.| * r) by XREAL_1: 68;

        (s + 0 ) < 1 by A3;

        then

         A8: (1 - s) > 0 by XREAL_1: 20;

        then 0 < |.(1 - s).| by ABSVALUE:def 1;

        then ( |.(1 - s).| * ||.(x - v).||) < ( |.(1 - s).| * r) by A6, XREAL_1: 68;

        then (( |.s.| * ||.(x - u).||) + ( |.(1 - s).| * ||.(x - v).||)) < (( |.s.| * r) + ( |.(1 - s).| * r)) by A7, XREAL_1: 8;

        then (( |.s.| * ||.(x - u).||) + ( |.(1 - s).| * ||.(x - v).||)) < ((s * r) + ( |.(1 - s).| * r)) by A2, ABSVALUE:def 1;

        then (( |.s.| * ||.(x - u).||) + ( |.(1 - s).| * ||.(x - v).||)) < ((s * r) + ((1 - s) * r)) by A8, ABSVALUE:def 1;

        then ( ||.(s * (x - u)).|| + ( |.(1 - s).| * ||.(x - v).||)) < (1 * r) by NORMSP_1:def 1;

        then

         A9: ( ||.(s * (x - u)).|| + ||.((1 - s) * (x - v)).||) < r by NORMSP_1:def 1;

         ||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| = ||.(((s * x) + ( - ((s * u) + ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:def 3

        .= ||.(((s * x) + (( - 1) * ((s * u) + ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1: 16

        .= ||.(((s * x) + ((( - 1) * (s * u)) + (( - 1) * ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:def 5

        .= ||.(((s * x) + (( - (s * u)) + (( - 1) * ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1: 16

        .= ||.(((s * x) + (( - (s * u)) + ( - ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1: 16

        .= ||.((((s * x) + ( - (s * u))) + ( - ((1 - s) * v))) + ((1 - s) * x)).|| by RLVECT_1:def 3

        .= ||.(((s * x) - (s * u)) + (((1 - s) * x) - ((1 - s) * v))).|| by RLVECT_1:def 3

        .= ||.((s * (x - u)) + (((1 - s) * x) - ((1 - s) * v))).|| by RLVECT_1: 34

        .= ||.((s * (x - u)) + ((1 - s) * (x - v))).|| by RLVECT_1: 34;

        then ||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| <= ( ||.(s * (x - u)).|| + ||.((1 - s) * (x - v)).||) by NORMSP_1:def 1;

        then ||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| < r by A9, XXREAL_0: 2;

        then ||.(((s + (1 - s)) * x) - ((s * u) + ((1 - s) * v))).|| < r by RLVECT_1:def 6;

        then ||.(x - ((s * u) + ((1 - s) * v))).|| < r by RLVECT_1:def 8;

        hence thesis;

      end;

      assume

       A10: V = ( Ball (x,r));

      for u,v be Point of ( LinearTopSpaceNorm X), s be Real st 0 < s & s < 1 & u in V & v in V holds ((s * u) + ((1 - s) * v)) in V

      proof

        let u,v be Point of ( LinearTopSpaceNorm X);

        let s be Real;

        reconsider u1 = u as Point of X by NORMSP_2:def 4;

        reconsider v1 = v as Point of X by NORMSP_2:def 4;

        (s * u1) = (s * u) & ((1 - s) * v1) = ((1 - s) * v) by NORMSP_2:def 4;

        then

         A11: ((s * u1) + ((1 - s) * v1)) = ((s * u) + ((1 - s) * v)) by NORMSP_2:def 4;

        assume 0 < s & s < 1 & u in V & v in V;

        hence thesis by A10, A1, A11;

      end;

      hence thesis;

    end;

    theorem :: LOPBAN_6:13

    

     Th13: for x be Point of X, r be Real, T be LinearOperator of X, Y, V be Subset of ( LinearTopSpaceNorm Y) st V = (T .: ( Ball (x,r))) holds V is convex

    proof

      let x be Point of X, r be Real, T be LinearOperator of X, Y, V be Subset of ( LinearTopSpaceNorm Y);

      reconsider V1 = (T .: ( Ball (x,r))) as Subset of Y;

      

       A1: for u,v be Point of Y, s be Real st 0 < s & s < 1 & u in V1 & v in V1 holds ((s * u) + ((1 - s) * v)) in V1

      proof

        reconsider Bxr = ( Ball (x,r)) as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        let u,v be Point of Y, s be Real;

        assume that

         A2: 0 < s & s < 1 and

         A3: u in V1 and

         A4: v in V1;

        consider z1 be object such that

         A5: z1 in the carrier of X and

         A6: z1 in ( Ball (x,r)) and

         A7: u = (T . z1) by A3, FUNCT_2: 64;

        reconsider zz1 = z1 as Point of X by A5;

        reconsider za1 = zz1 as Point of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        consider z2 be object such that

         A8: z2 in the carrier of X and

         A9: z2 in ( Ball (x,r)) and

         A10: v = (T . z2) by A4, FUNCT_2: 64;

        reconsider zz2 = z2 as Point of X by A8;

        

         A11: ((1 - s) * v) = (T . ((1 - s) * zz2)) by A10, LOPBAN_1:def 5;

        reconsider za2 = zz2 as Point of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        (s * za1) = (s * zz1) & ((1 - s) * za2) = ((1 - s) * zz2) by NORMSP_2:def 4;

        then

         A12: ((s * za1) + ((1 - s) * za2)) = ((s * zz1) + ((1 - s) * zz2)) by NORMSP_2:def 4;

        (s * u) = (T . (s * zz1)) by A7, LOPBAN_1:def 5;

        then

         A13: ((s * u) + ((1 - s) * v)) = (T . ((s * zz1) + ((1 - s) * zz2))) by A11, VECTSP_1:def 20;

        Bxr is convex by Th12;

        then ((s * za1) + ((1 - s) * za2)) in Bxr by A2, A6, A9;

        hence thesis by A12, A13, FUNCT_2: 35;

      end;

      assume

       A14: V = (T .: ( Ball (x,r)));

      for u,v be Point of ( LinearTopSpaceNorm Y), s be Real st 0 < s & s < 1 & u in V & v in V holds ((s * u) + ((1 - s) * v)) in V

      proof

        let u,v be Point of ( LinearTopSpaceNorm Y);

        let s be Real;

        reconsider u1 = u as Point of Y by NORMSP_2:def 4;

        reconsider v1 = v as Point of Y by NORMSP_2:def 4;

        (s * u1) = (s * u) & ((1 - s) * v1) = ((1 - s) * v) by NORMSP_2:def 4;

        then

         A15: ((s * u1) + ((1 - s) * v1)) = ((s * u) + ((1 - s) * v)) by NORMSP_2:def 4;

        assume 0 < s & s < 1 & u in V & v in V;

        hence thesis by A14, A1, A15;

      end;

      hence thesis;

    end;

    theorem :: LOPBAN_6:14

    

     Th14: for x be Point of X, r,s be Real st r <= s holds ( Ball (x,r)) c= ( Ball (x,s))

    proof

      let x be Point of X, r,s be Real;

      assume

       A1: r <= s;

      for u be Point of X st u in ( Ball (x,r)) holds u in ( Ball (x,s))

      proof

        let u be Point of X;

        assume u in ( Ball (x,r));

        then ex uu1 be Point of X st u = uu1 & ||.(x - uu1).|| < r;

        then ( ||.(x - u).|| + r) < (r + s) by A1, XREAL_1: 8;

        then ||.(x - u).|| < ((r + s) - r) by XREAL_1: 20;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: LOPBAN_6:15

    

     Th15: for X be RealBanachSpace, Y be RealNormSpace, T be Lipschitzian LinearOperator of X, Y, r be Real, BX1 be Subset of ( LinearTopSpaceNorm X), TBX1,BYr be Subset of ( LinearTopSpaceNorm Y) st r > 0 & BYr = ( Ball (( 0. Y),r)) & TBX1 = (T .: ( Ball (( 0. X),1))) & BYr c= ( Cl TBX1) holds BYr c= TBX1

    proof

      let X be RealBanachSpace, Y be RealNormSpace, T be Lipschitzian LinearOperator of X, Y, r be Real, BX1 be Subset of ( LinearTopSpaceNorm X), TBX1,BYr be Subset of ( LinearTopSpaceNorm Y);

      assume that

       A1: r > 0 and

       A2: BYr = ( Ball (( 0. Y),r)) and

       A3: TBX1 = (T .: ( Ball (( 0. X),1))) and

       A4: BYr c= ( Cl TBX1);

      

       A5: for x be Point of X, y be Point of Y, TB1,BYsr be Subset of ( LinearTopSpaceNorm Y), s be Real st s > 0 & TB1 = (T .: ( Ball (x,s))) & y = (T . x) & BYsr = ( Ball (y,(s * r))) holds BYsr c= ( Cl TB1)

      proof

        reconsider TB01 = (T .: ( Ball (( 0. X),1))) as Subset of Y;

        let x be Point of X, y be Point of Y, TB1,BYsr be Subset of ( LinearTopSpaceNorm Y), s be Real;

        assume that

         A6: s > 0 and

         A7: TB1 = (T .: ( Ball (x,s))) and

         A8: y = (T . x) and

         A9: BYsr = ( Ball (y,(s * r)));

        reconsider s1 = s as non zero Real by A6;

        reconsider y1 = y as Point of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

        

         A10: ( Ball (y,(s * r))) = (y + ( Ball (( 0. Y),(s * r)))) by Th2;

        reconsider TB0xs = (T .: ( Ball (x,s))) as Subset of Y;

        reconsider TB0s = (T .: ( Ball (( 0. X),s))) as Subset of Y;

        ( Ball (x,s)) = (x + ( Ball (( 0. X),s))) by Th2;

        then

         A11: (y + TB0s) = TB0xs by A8, Th6;

        (s1 * BYr) c= (s1 * ( Cl TBX1)) by A4, CONVEX1: 39;

        then (s1 * BYr) c= ( Cl (s1 * TBX1)) by RLTOPSP1: 52;

        then (y1 + (s1 * BYr)) c= (y1 + ( Cl (s1 * TBX1))) by RLTOPSP1: 8;

        then

         A12: (y1 + (s1 * BYr)) c= ( Cl (y1 + (s1 * TBX1))) by RLTOPSP1: 38;

        ( Ball (( 0. Y),(s * r))) = (s1 * ( Ball (( 0. Y),r))) by A6, Th3;

        then ( Ball (( 0. Y),(s * r))) = (s1 * BYr) by A2, Th9;

        then

         A13: (y1 + (s1 * BYr)) = BYsr by A9, A10, Th8;

        

         A14: (s1 * ( Ball (( 0. X),1))) = ( Ball (( 0. X),(s1 * 1))) by A6, Th3;

        (s1 * TB01) = (s1 * TBX1) by A3, Th9;

        hence thesis by A7, A12, A13, A11, A14, Th5, Th8;

      end;

      

       A15: for s0 be Real st s0 > 0 holds ( Ball (( 0. Y),r)) c= (T .: ( Ball (( 0. X),(1 + s0))))

      proof

        let s0 be Real;

        assume

         A16: s0 > 0 ;

        now

          let z be object;

          assume

           A17: z in ( Ball (( 0. Y),r));

          then

          reconsider y = z as Point of Y;

          consider s1 be Real such that

           A18: 0 < s1 and

           A19: s1 < s0 by A16, XREAL_1: 5;

          set a = (s1 / (1 + s1));

          set e = (a GeoSeq );

          

           A20: a < 1 by A18, XREAL_1: 29, XREAL_1: 191;

          then

           A21: |.a.| < 1 by A18, ABSVALUE:def 1;

          then

           A22: e is summable by SERIES_1: 24;

          defpred P[ Nat, Point of X, Point of X, Point of X] means $3 in ( Ball ($2,(e . $1))) & ||.((T . $3) - y).|| < ((e . ($1 + 1)) * r) implies $4 in ( Ball ($3,(e . ($1 + 1)))) & ||.((T . $4) - y).|| < ((e . ($1 + 2)) * r);

          reconsider B0 = ( Ball (y,((e . 1) * r))) as Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

          

           A23: 0 < a by A18, XREAL_1: 139;

          then (e . 1) = (a |^ 1) & 0 < (a |^ 1) by PREPOWER:def 1;

          then 0 < ((e . 1) * r) by A1, XREAL_1: 129;

          then ||.(y - y).|| < ((e . 1) * r) by NORMSP_1: 6;

          then B0 is open & y in B0 by NORMSP_2: 23;

          then ( Ball (y,((e . 1) * r))) meets TBX1 by A2, A4, A17, PRE_TOPC:def 7;

          then

          consider s be object such that

           A24: s in ( Ball (y,((e . 1) * r))) and

           A25: s in (T .: ( Ball (( 0. X),1))) by A3, XBOOLE_0: 3;

          consider xn1 be object such that

           A26: xn1 in the carrier of X and

           A27: xn1 in ( Ball (( 0. X),1)) and

           A28: s = (T . xn1) by A25, FUNCT_2: 64;

          reconsider xn1 as Point of X by A26;

          

           A29: for n be Nat holds for v,w be Point of X holds ex z be Point of X st P[n, v, w, z]

          proof

            let n be Nat;

            let v,w be Point of X;

            now

              reconsider B0 = ( Ball (y,((e . (n + 2)) * r))) as Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

              reconsider BYsr = ( Ball ((T . w),((e . (n + 1)) * r))) as Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

              reconsider TB1 = (T .: ( Ball (w,(e . (n + 1))))) as Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

              assume that w in ( Ball (v,(e . n))) and

               A30: ||.((T . w) - y).|| < ((e . (n + 1)) * r);

              (e . (n + 1)) = (a |^ (n + 1)) by PREPOWER:def 1;

              then

               A31: BYsr c= ( Cl TB1) by A5, A23, NEWTON: 83;

              (e . (n + 2)) = (a |^ (n + 2)) & 0 < (a |^ (n + 2)) by A23, NEWTON: 83, PREPOWER:def 1;

              then 0 < ((e . (n + 2)) * r) by A1, XREAL_1: 129;

              then ||.(y - y).|| < ((e . (n + 2)) * r) by NORMSP_1: 6;

              then

               A32: B0 is open & y in B0 by NORMSP_2: 23;

              y in BYsr by A30;

              then ( Ball (y,((e . (n + 2)) * r))) meets TB1 by A31, A32, PRE_TOPC:def 7;

              then

              consider s be object such that

               A33: s in ( Ball (y,((e . (n + 2)) * r))) and

               A34: s in (T .: ( Ball (w,(e . (n + 1))))) by XBOOLE_0: 3;

              consider z be object such that

               A35: z in the carrier of X and

               A36: z in ( Ball (w,(e . (n + 1)))) and

               A37: s = (T . z) by A34, FUNCT_2: 64;

              reconsider z as Point of X by A35;

              reconsider sb = (T . z) as Point of Y;

              ex ss1 be Point of Y st sb = ss1 & ||.(y - ss1).|| < ((e . (n + 2)) * r) by A33, A37;

              then ||.((T . z) - y).|| < ((e . (n + 2)) * r) by NORMSP_1: 7;

              hence ex z be Point of X st z in ( Ball (w,(e . (n + 1)))) & ||.((T . z) - y).|| < ((e . (n + 2)) * r) by A36;

            end;

            hence thesis;

          end;

          consider xn be sequence of X such that

           A38: (xn . 0 ) = ( 0. X) & (xn . 1) = xn1 & for n be Nat holds P[n, (xn . n), (xn . (n + 1)), (xn . (n + 2))] from RecExD3( A29);

          reconsider sb = (T . xn1) as Point of Y;

          

           A39: ex ss1 be Point of Y st sb = ss1 & ||.(y - ss1).|| < ((e . 1) * r) by A24, A28;

          

           A40: for n be Nat holds (xn . (n + 1)) in ( Ball ((xn . n),(e . n))) & ||.((T . (xn . (n + 1))) - y).|| < ((e . (n + 1)) * r)

          proof

            defpred PN[ Nat] means (xn . ($1 + 1)) in ( Ball ((xn . $1),(e . $1))) & ||.((T . (xn . ($1 + 1))) - y).|| < ((e . ($1 + 1)) * r);

             A41:

            now

              let n be Nat;

              assume

               A42: PN[n];

               P[n, (xn . n), (xn . (n + 1)), (xn . (n + 2))] by A38;

              hence PN[(n + 1)] by A42;

            end;

            

             A43: PN[ 0 ] by A27, A39, A38, NORMSP_1: 7, PREPOWER: 3;

            thus for n be Nat holds PN[n] from NAT_1:sch 2( A43, A41);

          end;

          

           A44: (e . 0 ) = 1 by PREPOWER: 3;

          

           A45: for m,k be Nat holds ||.((xn . (m + k)) - (xn . m)).|| <= ((e . m) * ((1 - (e . k)) / (1 - (e . 1))))

          proof

            let m be Nat;

            defpred PN[ Nat] means ||.((xn . (m + $1)) - (xn . m)).|| <= ((e . m) * ((1 - (e . $1)) / (1 - (e . 1))));

             A46:

            now

              let k be Nat;

              

               A47: ((((a |^ k) - (a |^ (k + 1))) / (1 - (a |^ 1))) + ((1 - (a |^ k)) / (1 - (a |^ 1)))) = ((((a |^ k) - (a |^ (k + 1))) + (1 - (a |^ k))) / (1 - (a |^ 1))) by XCMPLX_1: 62

              .= ((1 - (a |^ (k + 1))) / (1 - (a |^ 1)));

              assume PN[k];

              then ||.((xn . ((m + k) + 1)) - (xn . m)).|| <= ( ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ||.((xn . (m + k)) - (xn . m)).||) & ( ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ||.((xn . (m + k)) - (xn . m)).||) <= ( ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ((e . m) * ((1 - (e . k)) / (1 - (e . 1))))) by NORMSP_1: 10, XREAL_1: 6;

              then

               A48: ||.((xn . (m + (k + 1))) - (xn . m)).|| <= ( ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ((e . m) * ((1 - (e . k)) / (1 - (e . 1))))) by XXREAL_0: 2;

              (xn . ((m + k) + 1)) in ( Ball ((xn . (m + k)),(e . (m + k)))) by A40;

              then ex xn2 be Point of X st (xn . ((m + k) + 1)) = xn2 & ||.((xn . (m + k)) - xn2).|| < (e . (m + k));

              then ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| < (e . (m + k)) by NORMSP_1: 7;

              then

               A49: ( ||.((xn . ((m + k) + 1)) - (xn . (m + k))).|| + ((e . m) * ((1 - (e . k)) / (1 - (e . 1))))) <= ((e . (m + k)) + ((e . m) * ((1 - (e . k)) / (1 - (e . 1))))) by XREAL_1: 6;

              (a |^ 1) < 1 by A20;

              then 0 < (1 - (a |^ 1)) by XREAL_1: 50;

              

              then

               A50: (a |^ k) = (((a |^ k) * (1 - (a |^ 1))) / (1 - (a |^ 1))) by XCMPLX_1: 89

              .= (((a |^ k) - ((a |^ k) * (a |^ 1))) / (1 - (a |^ 1)))

              .= (((a |^ k) - (a |^ (k + 1))) / (1 - (a |^ 1))) by NEWTON: 8;

              ((e . (m + k)) + ((e . m) * ((1 - (e . k)) / (1 - (e . 1))))) = ((a |^ (m + k)) + ((e . m) * ((1 - (e . k)) / (1 - (e . 1))))) by PREPOWER:def 1

              .= ((a |^ (m + k)) + ((a |^ m) * ((1 - (e . k)) / (1 - (e . 1))))) by PREPOWER:def 1

              .= ((a |^ (m + k)) + ((a |^ m) * ((1 - (a |^ k)) / (1 - (e . 1))))) by PREPOWER:def 1

              .= ((a |^ (m + k)) + ((a |^ m) * ((1 - (a |^ k)) / (1 - (a |^ 1))))) by PREPOWER:def 1

              .= (((a |^ m) * (a |^ k)) + ((a |^ m) * ((1 - (a |^ k)) / (1 - (a |^ 1))))) by NEWTON: 8

              .= ((a |^ m) * ((1 - (a |^ (k + 1))) / (1 - (a |^ 1)))) by A50, A47

              .= ((e . m) * ((1 - (a |^ (k + 1))) / (1 - (a |^ 1)))) by PREPOWER:def 1

              .= ((e . m) * ((1 - (e . (k + 1))) / (1 - (a |^ 1)))) by PREPOWER:def 1

              .= ((e . m) * ((1 - (e . (k + 1))) / (1 - (e . 1)))) by PREPOWER:def 1;

              hence PN[(k + 1)] by A48, A49, XXREAL_0: 2;

            end;

             ||.((xn . (m + 0 )) - (xn . m)).|| = ||.( 0. X).|| by RLVECT_1: 5;

            then

             A51: PN[ 0 ] by A44;

            for k be Nat holds PN[k] from NAT_1:sch 2( A51, A46);

            hence thesis;

          end;

          

           A52: for k be Nat st 0 <= k holds ( ||.xn.|| . k) <= (1 / (1 - a))

          proof

            let k be Nat;

            assume 0 <= k;

            

             A53: (e . k) = (a |^ k) & (e . 1) = (a |^ 1) by PREPOWER:def 1;

            (a |^ 1) < 1 by A20;

            then

             A54: 0 < (1 - (a |^ 1)) by XREAL_1: 50;

            (1 - (a |^ k)) < 1 by A23, NEWTON: 83, XREAL_1: 44;

            then ((1 - (e . k)) / (1 - (e . 1))) <= (1 / (1 - (a |^ 1))) by A53, A54, XREAL_1: 74;

            then

             A55: ((1 - (e . k)) / (1 - (e . 1))) <= (1 / (1 - a));

             ||.((xn . ( 0 + k)) - (xn . 0 )).|| <= ((e . 0 ) * ((1 - (e . k)) / (1 - (e . 1)))) by A45;

            then ||.(xn . k).|| <= ((1 - (e . k)) / (1 - (e . 1))) by A44, A38, RLVECT_1: 13;

            then ||.(xn . k).|| <= (1 / (1 - a)) by A55, XXREAL_0: 2;

            hence thesis by NORMSP_0:def 4;

          end;

          

           A56: ( Sum e) = (1 / (1 - a)) by A21, SERIES_1: 24;

          (1 / (1 - a)) = (1 / (((1 * (1 + s1)) - s1) / (1 + s1))) by A18, XCMPLX_1: 127

          .= (1 + s1) by XCMPLX_1: 100;

          then

           A57: ( Sum e) < (1 + s0) by A19, A56, XREAL_1: 6;

          set xx = ( lim xn);

           A58:

          now

            let m be Nat;

            hereby

              let k be Nat;

              

               A59: 0 < (a |^ m) by A23, NEWTON: 83;

               ||.((xn . (m + k)) - (xn . m)).|| <= ((e . m) * ((1 - (e . k)) / (1 - (e . 1)))) by A45;

              then ||.((xn . (m + k)) - (xn . m)).|| <= ((a |^ m) * ((1 - (e . k)) / (1 - (e . 1)))) by PREPOWER:def 1;

              then ||.((xn . (m + k)) - (xn . m)).|| <= ((a |^ m) * ((1 - (a |^ k)) / (1 - (e . 1)))) by PREPOWER:def 1;

              then

               A60: ||.((xn . (m + k)) - (xn . m)).|| <= ((a |^ m) * ((1 - (a |^ k)) / (1 - (a |^ 1)))) by PREPOWER:def 1;

              (a |^ 1) < 1 by A20;

              then

               A61: 0 < (1 - (a |^ 1)) by XREAL_1: 50;

              (1 - (a |^ k)) < 1 by A23, NEWTON: 83, XREAL_1: 44;

              then ((1 - (a |^ k)) / (1 - (a |^ 1))) < (1 / (1 - (a |^ 1))) by A61, XREAL_1: 74;

              then ((a |^ m) * ((1 - (a |^ k)) / (1 - (a |^ 1)))) < ((a |^ m) * (1 / (1 - (a |^ 1)))) by A59, XREAL_1: 68;

              hence ||.((xn . (m + k)) - (xn . m)).|| < ((a |^ m) * (1 / (1 - (a |^ 1)))) by A60, XXREAL_0: 2;

            end;

          end;

          now

            let r1 be Real;

            

             A62: e is convergent & ( lim e) = 0 by A22, SERIES_1: 4;

            (a |^ 1) < 1 by A20;

            then

             A63: 0 < (1 - (a |^ 1)) by XREAL_1: 50;

            assume 0 < r1;

            then 0 < (r1 * (1 - (a |^ 1))) by A63, XREAL_1: 129;

            then

            consider p1 be Nat such that

             A64: for m be Nat st p1 <= m holds |.((e . m) - 0 ).| < (r1 * (1 - (a |^ 1))) by A62, SEQ_2:def 7;

            reconsider p1 as Nat;

            take m = p1;

             |.((e . p1) - 0 ).| < (r1 * (1 - (a |^ 1))) by A64;

            then (e . p1) < ( 0 + (r1 * (1 - (a |^ 1)))) by RINFSUP1: 1;

            then ((e . p1) / (1 - (a |^ 1))) < ((r1 * (1 - (a |^ 1))) / (1 - (a |^ 1))) by A63, XREAL_1: 74;

            then ((e . p1) / (1 - (a |^ 1))) < r1 by A63, XCMPLX_1: 89;

            then ((a |^ p1) / (1 - (a |^ 1))) < r1 by PREPOWER:def 1;

            then

             A65: ((a |^ p1) * (1 / (1 - (a |^ 1)))) < r1 by XCMPLX_1: 99;

            hereby

              let n be Nat;

              assume m <= n;

              then

              consider k1 be Nat such that

               A66: n = (m + k1) by NAT_1: 10;

              reconsider k1 as Nat;

              n = (m + k1) by A66;

              hence ||.((xn . n) - (xn . m)).|| < r1 by A58, A65, XXREAL_0: 2;

            end;

          end;

          then xn is Cauchy_sequence_by_Norm by LOPBAN_3: 5;

          then

           A67: xn is convergent by LOPBAN_1:def 15;

          then ( lim ||.xn.||) = ||.( lim xn).|| by LOPBAN_1: 41;

          then ||.xx.|| <= ( Sum e) by A56, A67, A52, LOPBAN_1: 41, RSSPACE2: 5;

          then ||.xx.|| < (1 + s0) by A57, XXREAL_0: 2;

          then ||.( - xx).|| < (1 + s0) by NORMSP_1: 2;

          then ||.(( 0. X) - xx).|| < (1 + s0) by RLVECT_1: 14;

          then

           A68: xx in ( Ball (( 0. X),(1 + s0)));

          ( rng xn) c= the carrier of X;

          then

           A69: ( rng xn) c= ( dom T) by FUNCT_2:def 1;

           A70:

          now

            let n be Nat;

            

             A71: n in NAT by ORDINAL1:def 12;

            

            thus ((T /* xn) . n) = (T /. (xn . n)) by A69, FUNCT_2: 109, A71

            .= (T . (xn . n));

          end;

           A72:

          now

            let s be Real;

            assume 0 < s;

            then

             A73: 0 < (s / r) by A1, XREAL_1: 139;

            e is convergent & ( lim e) = 0 by A22, SERIES_1: 4;

            then

            consider m0 be Nat such that

             A74: for n be Nat st m0 <= n holds |.((e . n) - 0 ).| < (s / r) by A73, SEQ_2:def 7;

            reconsider m = (m0 + 1) as Nat;

            take m;

            (a |^ 1) < 1 & 0 < (a |^ m0) by A23, A20, NEWTON: 83;

            then ((a |^ m0) * (a |^ 1)) <= (a |^ m0) by XREAL_1: 153;

            then (a |^ (m0 + 1)) <= (a |^ m0) by NEWTON: 8;

            then (e . (m0 + 1)) <= (a |^ m0) by PREPOWER:def 1;

            then

             A75: (e . (m0 + 1)) <= (e . m0) by PREPOWER:def 1;

             |.((e . m0) - 0 ).| < (s / r) by A74;

            then (e . m0) < ( 0 + (s / r)) by RINFSUP1: 1;

            then (e . (m0 + 1)) < (s / r) by A75, XXREAL_0: 2;

            then ((e . (m0 + 1)) * r) < ((s / r) * r) by A1, XREAL_1: 68;

            then

             A76: ((e . (m0 + 1)) * r) < s by A1, XCMPLX_1: 87;

            now

              let n be Nat;

              assume

               A77: m <= n;

              1 <= (m0 + 1) by NAT_1: 11;

              then

              reconsider n0 = (n - 1) as Nat by A77, NAT_1: 21, XXREAL_0: 2;

              consider m1 be Nat such that

               A78: (n0 + 1) = ((m0 + 1) + m1) by A77, NAT_1: 10;

              

               A79: (a |^ (n0 + 1)) = ((a |^ (m0 + 1)) * (a |^ m1)) by A78, NEWTON: 8;

               0 < (a |^ (m0 + 1)) & (a |^ m1) <= (1 |^ m1) by A23, A20, NEWTON: 83, PREPOWER: 9;

              then (a |^ (n0 + 1)) <= (a |^ (m0 + 1)) by A79, XREAL_1: 153;

              then (e . (n0 + 1)) <= (a |^ (m0 + 1)) by PREPOWER:def 1;

              then (e . (n0 + 1)) <= (e . (m0 + 1)) by PREPOWER:def 1;

              then ((e . (n0 + 1)) * r) <= ((e . (m0 + 1)) * r) by A1, XREAL_1: 64;

              then ||.((T . (xn . n)) - y).|| <= ((e . (m0 + 1)) * r) by A40, XXREAL_0: 2;

              then ||.((T . (xn . n)) - y).|| < s by A76, XXREAL_0: 2;

              hence ||.(((T /* xn) . n) - y).|| < s by A70;

            end;

            hence for n be Nat st m <= n holds ||.(((T /* xn) . n) - y).|| < s;

          end;

          T is_continuous_in xx by LOPBAN_5: 4;

          then (T /* xn) is convergent & (T /. xx) = ( lim (T /* xn)) by A67, A69, NFCONT_1:def 5;

          then y = (T . xx) by A72, NORMSP_1:def 7;

          hence z in (T .: ( Ball (( 0. X),(1 + s0)))) by A68, FUNCT_2: 35;

        end;

        hence thesis;

      end;

      now

        reconsider TB01 = (T .: ( Ball (( 0. X),1))) as Subset of Y;

        let z be object;

        assume

         A80: z in ( Ball (( 0. Y),r));

        then

        reconsider y = z as Point of Y;

        ex yy1 be Point of Y st y = yy1 & ||.(( 0. Y) - yy1).|| < r by A80;

        then ||.( - y).|| < r by RLVECT_1: 14;

        then

         A81: ||.y.|| < r by NORMSP_1: 2;

        consider s0 be Real such that

         A82: 0 < s0 and

         A83: ||.y.|| < (r / (1 + s0)) and (r / (1 + s0)) < r by A81, Th1;

        set y1 = ((1 + s0) * y);

        ((1 + s0) * ||.y.||) < ((r / (1 + s0)) * (1 + s0)) by A82, A83, XREAL_1: 68;

        then ((1 + s0) * ||.y.||) < r by A82, XCMPLX_1: 87;

        then ( |.(1 + s0).| * ||.y.||) < r by A82, ABSVALUE:def 1;

        then ||.((1 + s0) * y).|| < r by NORMSP_1:def 1;

        then ||.( - y1).|| < r by NORMSP_1: 2;

        then ||.(( 0. Y) - y1).|| < r by RLVECT_1: 14;

        then

         A84: ((1 + s0) * y) in ( Ball (( 0. Y),r));

        ( Ball (( 0. Y),r)) c= (T .: ( Ball (( 0. X),(1 + s0)))) by A15, A82;

        then

         A85: ((1 + s0) * y) in (T .: ( Ball (( 0. X),(1 + s0)))) by A84;

        reconsider s1 = (1 + s0) as non zero Real by A82;

        (s1 * ( Ball (( 0. X),1))) = ( Ball (( 0. X),(s1 * 1))) by A82, Th3;

        then (s1 * y) in (s1 * TB01) by A85, Th5;

        then ((s1 " ) * (s1 * y)) in ((s1 " ) * (s1 * TB01));

        then (((s1 " ) * s1) * y) in ((s1 " ) * (s1 * TB01)) by RLVECT_1:def 7;

        then

         A86: (((s1 " ) * s1) * y) in (((s1 " ) * s1) * TB01) by CONVEX1: 37;

        ((s1 " ) * s1) = ((1 / s1) * s1) by XCMPLX_1: 215

        .= 1 by XCMPLX_1: 106;

        then y in (1 * TB01) by A86, RLVECT_1:def 8;

        hence z in (T .: ( Ball (( 0. X),1))) by CONVEX1: 32;

      end;

      hence thesis by A2, A3;

    end;

    ::$Notion-Name

    theorem :: LOPBAN_6:16

    for X,Y be RealBanachSpace, T be Lipschitzian LinearOperator of X, Y, T1 be Function of ( LinearTopSpaceNorm X), ( LinearTopSpaceNorm Y) st T1 = T & T1 is onto holds T1 is open

    proof

      let X,Y be RealBanachSpace, T be Lipschitzian LinearOperator of X, Y, T1 be Function of ( LinearTopSpaceNorm X), ( LinearTopSpaceNorm Y);

      assume that

       A1: T1 = T and

       A2: T1 is onto;

      thus for G be Subset of ( LinearTopSpaceNorm X) st G is open holds (T1 .: G) is open

      proof

        reconsider TB1 = (T .: ( Ball (( 0. X),1))) as Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

        defpred P[ Nat, set] means ex TBn be Subset of ( TopSpaceNorm Y) st TBn = (T .: ( Ball (( 0. X),$1))) & $2 = ( Cl TBn);

        let G be Subset of ( LinearTopSpaceNorm X);

        

         A3: for n be Element of NAT holds ex y be Element of ( bool the carrier of Y) st P[n, y]

        proof

          let n be Element of NAT ;

          reconsider TBn = (T .: ( Ball (( 0. X),n))) as Subset of ( TopSpaceNorm Y);

          ( Cl TBn) c= the carrier of Y;

          hence thesis;

        end;

        consider f be sequence of ( bool the carrier of Y) such that

         A4: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

        reconsider f as SetSequence of Y;

        

         A5: for n be Nat holds (f . n) is closed

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then ex TBn be Subset of ( TopSpaceNorm Y) st TBn = (T .: ( Ball (( 0. X),n))) & (f . n) = ( Cl TBn) by A4;

          hence thesis by NORMSP_2: 15;

        end;

        

         A6: the carrier of Y c= ( union ( rng f))

        proof

          let z be object;

          assume z in the carrier of Y;

          then

          reconsider z1 = z as Point of Y;

          ( rng T) = the carrier of ( LinearTopSpaceNorm Y) by A1, A2, FUNCT_2:def 3;

          then ( rng T) = the carrier of Y by NORMSP_2:def 4;

          then

          consider x1 be object such that

           A7: x1 in the carrier of X and

           A8: z1 = (T . x1) by FUNCT_2: 11;

          reconsider x1 as Point of X by A7;

          consider m be Element of NAT such that

           A9: ||.x1.|| <= m by MESFUNC1: 8;

          set n = (m + 1);

          ( ||.x1.|| + 0 ) < (m + 1) by A9, XREAL_1: 8;

          then ||.( - x1).|| < n by NORMSP_1: 2;

          then ||.(( 0. X) - x1).|| < n by RLVECT_1: 14;

          then x1 in ( Ball (( 0. X),n));

          then

           A10: (T . x1) in (T .: ( Ball (( 0. X),n))) by FUNCT_2: 35;

           NAT = ( dom f) by FUNCT_2:def 1;

          then

           A11: (f . n) in ( rng f) by FUNCT_1: 3;

          consider TBn be Subset of ( TopSpaceNorm Y) such that

           A12: TBn = (T .: ( Ball (( 0. X),n))) and

           A13: (f . n) = ( Cl TBn) by A4;

          TBn c= (f . n) by A13, PRE_TOPC: 18;

          hence thesis by A8, A10, A12, A11, TARSKI:def 4;

        end;

        ( union ( rng f)) is Subset of Y by PROB_1: 11;

        then ( union ( rng f)) = the carrier of Y by A6;

        then

        consider n0 be Nat, r be Real, y0 be Point of Y such that

         A14: 0 < r and

         A15: ( Ball (y0,r)) c= (f . n0) by A5, LOPBAN_5: 3;

        n0 in NAT by ORDINAL1:def 12;

        then

        consider TBn0 be Subset of ( TopSpaceNorm Y) such that

         A16: TBn0 = (T .: ( Ball (( 0. X),n0))) and

         A17: (f . n0) = ( Cl TBn0) by A4;

        consider TBn01 be Subset of ( TopSpaceNorm Y) such that

         A18: TBn01 = (T .: ( Ball (( 0. X),(n0 + 1)))) and

         A19: (f . (n0 + 1)) = ( Cl TBn01) by A4;

        ( Ball (( 0. X),n0)) c= ( Ball (( 0. X),(n0 + 1))) by Th14, NAT_1: 11;

        then TBn0 c= TBn01 by A16, A18, RELAT_1: 123;

        then (f . n0) c= (f . (n0 + 1)) by A17, A19, PRE_TOPC: 19;

        then

         A20: ( Ball (y0,r)) c= ( Cl TBn01) by A15, A19;

        reconsider LTBn01 = TBn01 as Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

        ( - 1) is non zero Real;

        then

         A21: ( Cl (( - 1) * LTBn01)) = (( - 1) * ( Cl LTBn01)) by RLTOPSP1: 52;

        reconsider yy0 = y0 as Point of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

        

         A22: ( Ball (( 0. Y),(r / ((2 * n0) + 2)))) is Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

         ||.(y0 - y0).|| < r by A14, NORMSP_1: 6;

        then y0 in ( Ball (y0,r));

        then y0 in ( Cl TBn01) by A20;

        then yy0 in ( Cl LTBn01) by Th10;

        then

         A23: (( - 1) * yy0) in (( - 1) * ( Cl LTBn01));

        reconsider nb1 = (1 / ((2 * n0) + 2)) as non zero Real by XREAL_1: 139;

        reconsider TBX1 = (T .: ( Ball (( 0. X),1))) as Subset of Y;

        reconsider my0 = {( - yy0)} as Subset of ( LinearTopSpaceNorm Y);

        reconsider TBnx01 = (T .: ( Ball (( 0. X),(n0 + 1)))) as Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

        reconsider BYyr = ( Ball (y0,r)) as Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

        reconsider BYr = ( Ball (( 0. Y),r)) as Subset of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

        reconsider XTB01 = (T .: ( Ball (( 0. X),(n0 + 1)))) as Subset of Y;

        

         A24: ( - yy0) = (( - 1) * yy0) by RLVECT_1: 16

        .= (( - 1) * y0) by NORMSP_2:def 4

        .= ( - y0) by RLVECT_1: 16;

        (( - 1) * LTBn01) = (( - 1) * XTB01) by A18, Th9

        .= (T .: (( - 1) * ( Ball (( 0. X),(n0 + 1))))) by Th5

        .= LTBn01 by A18, Th11;

        then ( - yy0) in ( Cl LTBn01) by A21, A23, RLVECT_1: 16;

        then ( - yy0) in ( Cl TBn01) by Th10;

        then {( - yy0)} c= ( Cl TBn01) by ZFMISC_1: 31;

        then

         A25: my0 c= ( Cl TBnx01) by A18, Th10;

        BYyr c= ( Cl TBnx01) by A18, A20, Th10;

        then (my0 + BYyr) c= (( Cl TBnx01) + ( Cl TBnx01)) by A25, RLTOPSP1: 11;

        then (( - yy0) + BYyr) c= (( Cl TBnx01) + ( Cl TBnx01)) by RUSUB_4: 33;

        then

         A26: (( - y0) + ( Ball (y0,r))) c= (( Cl TBnx01) + ( Cl TBnx01)) by A24, Th8;

        

         A27: (( Cl TBnx01) + ( Cl TBnx01)) c= ( Cl (TBnx01 + TBnx01)) by RLTOPSP1: 62;

        ( Ball (y0,r)) = (y0 + ( Ball (( 0. Y),r))) by Th2;

        then BYyr = (yy0 + BYr) by Th8;

        then (( - yy0) + BYyr) = ((( - yy0) + yy0) + BYr) by RLTOPSP1: 6;

        then (( - yy0) + BYyr) = (( 0. ( LinearTopSpaceNorm Y)) + BYr) by RLVECT_1: 5;

        then (( - yy0) + BYyr) = ( {( 0. ( LinearTopSpaceNorm Y))} + BYr) by RUSUB_4: 33;

        then (( - yy0) + BYyr) = BYr by CONVEX1: 35;

        then ( Ball (( 0. Y),r)) = (( - y0) + ( Ball (y0,r))) by A24, Th8;

        then

         A28: ( Ball (( 0. Y),r)) c= ( Cl (TBnx01 + TBnx01)) by A26, A27;

        TBnx01 = (1 * TBnx01) by CONVEX1: 32;

        

        then

         A29: (TBnx01 + TBnx01) = ((1 + 1) * TBnx01) by Th13, CONVEX1: 13

        .= (2 * TBnx01);

        ( Ball (( 0. X),((n0 + 1) * 1))) = ((n0 + 1) * ( Ball (( 0. X),1))) by Th3;

        then ((n0 + 1) * TBX1) = (T .: ( Ball (( 0. X),(n0 + 1)))) by Th5;

        

        then (TBnx01 + TBnx01) = (2 * ((n0 + 1) * TB1)) by A29, Th9

        .= ((2 * (n0 + 1)) * TB1) by CONVEX1: 37

        .= (((2 * n0) + 2) * TB1);

        then

         A30: ( Cl (TBnx01 + TBnx01)) = (((2 * n0) + 2) * ( Cl TB1)) by RLTOPSP1: 52;

        

         A31: 0 < (r / ((2 * n0) + 2)) by A14, XREAL_1: 139;

        ( Ball (( 0. Y),(r / ((2 * n0) + 2)))) = ( Ball (( 0. Y),((r * 1) / ((2 * n0) + 2))))

        .= ( Ball (( 0. Y),(r * (1 / ((2 * n0) + 2))))) by XCMPLX_1: 74

        .= (nb1 * ( Ball (( 0. Y),r))) by Th3

        .= (nb1 * BYr) by Th9;

        then

         A32: ( Ball (( 0. Y),(r / ((2 * n0) + 2)))) c= ((1 / ((2 * n0) + 2)) * (((2 * n0) + 2) * ( Cl TB1))) by A28, A30, CONVEX1: 39;

        ((1 / ((2 * n0) + 2)) * (((2 * n0) + 2) * ( Cl TB1))) = (((1 / ((2 * n0) + 2)) * ((2 * n0) + 2)) * ( Cl TB1)) by CONVEX1: 37

        .= (1 * ( Cl TB1)) by XCMPLX_1: 106

        .= ( Cl TB1) by CONVEX1: 32;

        then

         A33: ( Ball (( 0. Y),(r / ((2 * n0) + 2)))) c= (T .: ( Ball (( 0. X),1))) by A14, A32, A22, Th15, XREAL_1: 139;

        

         A34: for p be Real st p > 0 holds ex q be Real st 0 < q & ( Ball (( 0. Y),q)) c= (T .: ( Ball (( 0. X),p)))

        proof

          reconsider TB1 = (T .: ( Ball (( 0. X),1))) as Subset of Y;

          let p be Real;

          assume

           A35: p > 0 ;

          then

           A36: (p * ( Ball (( 0. X),1))) = ( Ball (( 0. X),(p * 1))) by Th3;

          take ((r / ((2 * n0) + 2)) * p);

          (p * ( Ball (( 0. Y),(r / ((2 * n0) + 2))))) c= (p * TB1) by A33, CONVEX1: 39;

          then ( Ball (( 0. Y),((r / ((2 * n0) + 2)) * p))) c= (p * TB1) by A35, Th3;

          hence thesis by A31, A35, A36, Th5, XREAL_1: 129;

        end;

        assume

         A37: G is open;

        now

          let y be Point of Y;

          assume y in (T1 .: G);

          then

          consider x be Point of X such that

           A38: x in G and

           A39: y = (T . x) by A1, FUNCT_2: 65;

          consider p be Real such that

           A40: p > 0 and

           A41: { z where z be Point of X : ||.(x - z).|| < p } c= G by A37, A38, NORMSP_2: 22;

          reconsider TBp = (T .: ( Ball (( 0. X),p))) as Subset of Y;

          consider q be Real such that

           A42: 0 < q and

           A43: ( Ball (( 0. Y),q)) c= TBp by A34, A40;

          ( Ball (x,p)) c= G by A41;

          then

           A44: (x + ( Ball (( 0. X),p))) c= G by Th2;

          now

            let t be object;

            assume t in (y + TBp);

            then

            consider tz0 be Point of Y such that

             A45: t = (y + tz0) and

             A46: tz0 in TBp;

            consider z0 be Element of X such that

             A47: z0 in ( Ball (( 0. X),p)) and

             A48: tz0 = (T . z0) by A46, FUNCT_2: 65;

            reconsider z0 as Point of X;

            

             A49: (x + z0) in (x + ( Ball (( 0. X),p))) by A47;

            t = (T . (x + z0)) by A39, A45, A48, VECTSP_1:def 20;

            hence t in (T1 .: G) by A1, A44, A49, FUNCT_2: 35;

          end;

          then

           A50: (y + TBp) c= (T .: G) by A1;

          take q;

          now

            let t be object;

            assume t in (y + ( Ball (( 0. Y),q)));

            then ex z0 be Point of Y st t = (y + z0) & z0 in ( Ball (( 0. Y),q));

            hence t in (y + TBp) by A43;

          end;

          then (y + ( Ball (( 0. Y),q))) c= (y + TBp);

          then ( Ball (y,q)) c= (y + TBp) by Th2;

          hence 0 < q & { w where w be Point of Y : ||.(y - w).|| < q } c= (T1 .: G) by A1, A50, A42;

        end;

        hence thesis by NORMSP_2: 22;

      end;

    end;