:: Open Mapping Theorem
::  by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
:: 
:: Received September 23, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies TARSKI, BOOLE, RLVECT_1, FUNCT_1, PRE_TOPC, ARYTM, ABSVALUE,
      ARYTM_1, FCONT_1, FINSEQ_4, ARYTM_3, RELAT_1, SEQ_2, LATTICES, OPPCAT_1,
      ORDINAL2, NORMSP_1, PREPOWER, METRIC_1, NORMSP_2, PROB_1, RSSPACE3,
      LOPBAN_1, SUPINF_2, JORDAN1, MCART_1, GROUP_1, XREAL_0, SGRAPH1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, RELSET_1,
      FUNCT_2, PARTFUN1, MCART_1, FUNCOP_1, PRE_TOPC, DOMAIN_1, BINOP_1,
      ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1,
      STRUCT_0, XXREAL_0, SEQ_1, SEQ_2, INT_1, NEWTON, PREPOWER, SERIES_1,
      RLVECT_1, FRAENKEL, CONVEX1, METRIC_1, RUSUB_4, NORMSP_1, NORMSP_2,
      RSSPACE3, RLTOPSP1, LOPBAN_1, NFCONT_1, LOPBAN_5, KURATO_2, T_0TOPSP;
 constructors XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL2, TOPS_1, REAL_1, DOMAIN_1,
      SEQ_1, SEQ_2, PCOMPS_1, RUSUB_4, CONVEX1, RLTOPSP1, NFCONT_1, NAT_1,
      FUNCT_1, FUNCT_2, PSCOMP_1, PARTFUN1, NEWTON, PREPOWER, SERIES_1,
      NORMSP_2, RSSPACE3, LOPBAN_1, LOPBAN_5, T_0TOPSP;
 registrations REAL_1, NUMBERS, ORDINAL2, XREAL_0, ZFMISC_1, XBOOLE_0,
      METRIC_1, SERIES_1, XXREAL_0, ORDINAL1, RELSET_1, STRUCT_0, MEMBERED,
      RLTOPSP1, TOPS_1, KURATO_2, SUBSET_1, NAT_1, RLVECT_1, NORMSP_1,
      NORMSP_2, FUNCT_1, FUNCT_2, FUNCOP_1, RSSPACE3, SEQM_3, PARTFUN1,
      MONOID_0, PROB_1, LOPBAN_1, LOPBAN_5, T_0TOPSP;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, RLVECT_1, METRIC_1, PCOMPS_1, CONVEX1, RUSUB_4, T_0TOPSP,
      XREAL_0, RLSUB_1, ALGSTR_0, ZFMISC_1, RLTOPSP1, NORMSP_2, XBOOLE_0,
      RSSPACE3, ORDINAL1, BHSP_1, SEQ_2, SERIES_1, PREPOWER, SUBSET_1,
      FRAENKEL, LOPBAN_1, LOPBAN_5, NFCONT_1, MEMBERED, FUNCT_1, FUNCT_2;
 theorems TARSKI, XBOOLE_1, SEQ_2, RLVECT_1, XREAL_0, RELAT_1, RUSUB_4,
      RLTOPSP1, SERIES_1, PREPOWER, ZFMISC_1, FUNCT_2, XBOOLE_0, XREAL_1,
      XCMPLX_1, NORMSP_1, PRE_TOPC, NFCONT_1, XXREAL_0, FUNCT_1, NEWTON,
      MESFUNC1, NORMSP_2, RINFSUP1, ABSVALUE, XCMPLX_0, LOPBAN_3, ORDINAL1,
      SUBSET_1, RSSPACE2, LOPBAN_1, NAT_1, REAL_2, PROB_1, LOPBAN_5, CONVEX1,
      MCART_1;
 schemes FUNCT_2, RECDEF_1, NAT_1;

begin

theorem Lm00:
 for x,y be real number st 0<=x & x<y
   ex s0 be real number st 0<s0 & x < y/(1+s0) & y/(1+s0) < y
   proof
   let x,y be real number;
   assume AS0: 0<=x & x<y;
    ex s0 be real number st
    0<s0 & x < y/(1+s0) & y/(1+s0) < y
     proof
        consider s be real number such that
     X1: x < s & s < y by XREAL_1:7,AS0;
      now per cases by AS0;
   case XK0: 0=x;
         set s0=s;
      y < y*(1+s0) by X1,AS0,XREAL_1:31,XREAL_1:157;
    hence 0<s0 & x < y/(1+s0) & y/(1+s0) < y
                 by X1,XK0,XREAL_1:141,XREAL_1:85;
   end;
    case XK1: 0<x;
          set s0=s /x - 1;
         RX2:0 < 1+s0 & 1< 1+s0 by XREAL_1:189,X1,XK1;
          (1+s0)*x=(x/x)*s by XCMPLX_1:76;
           then (1+s0)*x=1*s by XCMPLX_1:60,XK1;
           then
         RX3:(1+s0)"*(1+s0)*x=s*(1+s0)";
         LV1:(1+s0)"=1/(1+s0) by XCMPLX_1:217;
         LV3:(1+s0)"*(1+s0)=1 by LV1,XCMPLX_1:107,RX2;
         LV5:s*(1+s0)"= (s*1)/(1+s0) by LV1,XCMPLX_1:75;
              y < y*(1+s0) by AS0,RX2,XREAL_1:157;
       hence 0<s0 & x < y/(1+s0) & y/(1+s0) < y
           by XREAL_1:52,XREAL_1:85,RX2,X1,RX3,LV3,LV5,XREAL_1:76;
    end;
    end;
     hence thesis;
    end;
     hence thesis;
   end;

scheme RecExD3{D() -> non empty set, A() -> Element of D(),
            B() -> Element of D(), P[set,set,set,set]}:
   ex f being Function of NAT,D() st
     f.0 = A() & f.1 = B() &
     for n being Element of NAT holds P[n,f.n,f.(n+1),f.(n+2)]
 provided
  P0:  for n being Element of NAT for x,y being Element of D()
       ex z being Element of D() st P[n,x,y,z]
 proof
 defpred Q[set,set,set]
   means
     P[$1, $2`1,$2`2, $3`2] & $2`2 = $3`1;
 P1:  for n being Element of NAT for x being Element of [:D(),D() :]
       ex y being Element of [:D(),D() :]
          st Q[n,x,y]
 proof
    let n be Element of 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 being Element of D() such that
      P2: P[n,z,w,s] by P0;
      set y = [w,s];
      reconsider y as Element of [:D(),D() :];
      take y;
       thus Q[n,x,y] by P2,MCART_1:7;
   end;
 consider g being Function of NAT,[:D(),D() :] such that
  P2:     g.0 = [A(),B()] &
       for n being Element of NAT holds Q[n,g.n,g.(n+1)]
  from RECDEF_1:sch 2(P1);
  deffunc F(Element of NAT)=(g.$1)`1;
  P3: for x being Element of NAT holds F(x) in D();
  consider f being Function of NAT,D() such that
  P4: for x being Element of NAT holds f.x = F(x)
   from FUNCT_2:sch 8(P3);
  take f;
  P5:Q[0,g.0,g.(0+1)] by P2;
  EA1: f.0 = (g.0)`1 by P4
          .= A() by MCART_1:7,P2;
  EA2: f.1 = (g.1)`1 by P4
          .= B() by MCART_1:7,P2,P5;
   now let n be Element of NAT;
   P6:Q[n+1,g.(n+1),g.((n+1)+1)] by P2;
   E1: f.n = (g.n)`1 by P4;
   E2: f.(n+1) = (g.(n+1))`1 by P4
              .=(g.n)`2 by P2;
   f.(n+2) =(g.(n+1))`2 by P6,P4;
  hence P[n, f.n,f.(n+1), f.(n+2)] by P2,E1,E2;
   end;
  hence thesis by EA1,EA2;
  end;

 reserve X, Y for RealNormSpace;

theorem Lm01:
  for y1 be Point of X, r be real number
    holds Ball(y1,r) = y1 + Ball(0.X,r)
   proof
    let y1 be Point of X, r be real number;
    thus Ball(y1,r) c=y1 + Ball(0.X,r)
   proof
  let t be set;
  assume A1: t in Ball(y1,r);
  reconsider z1=t as Point of X by A1;
  set z0=z1-y1;
  ex zz1 be Point of X st z1=zz1 & ||.y1-zz1.|| < r by A1;
  then ||.-z0.|| < r by RLVECT_1:47;
  then ||.0.X-z0.||< r by RLVECT_1:27;
  then
  A2: z0 in Ball(0.X,r);
   z0+y1=z1+((-y1)+y1) by RLVECT_1:def 6;
   then z0+y1=z1+0.X by RLVECT_1:16;
   then z1=z0+y1 by RLVECT_1:10;
   hence t in y1 + Ball(0.X,r) by A2;
 end;
  let t be set;
  assume t in y1 + Ball(0.X,r);
  then consider z0 be Point of X such that
  B1: t=y1+z0 & z0 in Ball(0.X,r);
  set z1=z0+y1;
    ex zz0 be Point of X st
     z0=zz0 & ||.0.X-zz0.|| < r by B1;
      then ||.-z0.|| < r by RLVECT_1:27;
      then ||.z0.|| < r by NORMSP_1:6;
      then ||.z0+ 0.X.|| < r by RLVECT_1:10;
      then ||.z0+ (y1+-y1).|| < r by RLVECT_1:16;
      then ||.z1-y1.|| < r by RLVECT_1:def 6;
      then ||.y1-z1.|| < r by NORMSP_1:11;
      hence t in Ball(y1,r) by B1;
     end;

theorem Lm02:
  for r be real number, a be Real st 0 < a
    holds Ball(0.X,a*r) = a * Ball(0.X,r)
   proof
   let r be real number, a be Real;
   assume AS: 0 < a;
   thus Ball(0.X,a*r) c= a * Ball(0.X,r)
   proof
   let z be set;
    assume
    R1: 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 R1;
    then ||.-z1.|| < a*r by RLVECT_1:27;
    then
    R2: ||.z1.|| < a*r by NORMSP_1:6;
   set y1=a"*z1;
    R4: ||.y1.|| = abs(a")* ||.z1.|| by NORMSP_1:def 2
                .= a"* ||.z1.|| by AS, ABSVALUE:def 1;
    a"* ||.z1.|| < a"* (a*r) by R2,AS,XREAL_1:70;
    then a"* ||.z1.|| < (a*a")*r;
    then a"* ||.z1.|| < 1*r by XCMPLX_0:def 7,AS;
    then ||.-y1.|| < r by NORMSP_1:6,R4;
    then ||.0.X-y1.|| < r by RLVECT_1:27;
    then
    RA1: y1 in Ball(0.X,r);
     a*y1=a*a"*z1 by RLVECT_1:def 9
        .= 1*z1 by XCMPLX_0:def 7,AS
        .= z1 by RLVECT_1:def 9;
    hence z in a * Ball(0.X,r) by RA1;
    end;
  let z be set;
  assume
  L1: z in a*Ball(0.X,r);
   reconsider z1 = z as Point of X by L1;
    consider y1 be Point of X such that
   B1: z1=a * y1 & y1 in Ball(0.X,r) by L1;
     ex yy1 be Point of X st
       y1=yy1 & ||.0.X-yy1.||<r by B1;
    then ||.-y1.|| < r by RLVECT_1:27;
    then
 R2: ||.y1.|| < r by NORMSP_1:6;
     ||.z1.|| = abs(a)* ||.y1.|| by B1,NORMSP_1:def 2
             .= a* ||.y1.|| by AS, ABSVALUE:def 1;
    then ||.z1.|| < a*r by R2,AS,XREAL_1:70;
    then ||.-z1.|| < a*r by NORMSP_1:6;
    then ||.0.X-z1.|| < a*r by RLVECT_1:27;
     hence z in Ball(0.X,a*r);
    end;

theorem
  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 set;
     assume t in T.:(B0+B1);
     then
     consider z1 be set such that
     A1: z1 in the carrier of X & z1 in B0+B1
      & t= T.z1 by FUNCT_2:115;
   consider x1,x2 be Element of X such that
   A3: z1=x1+x2 & x1 in B0 & x2 in B1 by A1;
   A4: t=T.x1+T.x2 by LOPBAN_1:def 5,A1,A3;
   A5:T.x1 in T.:B0 by A3,FUNCT_2:43;
      T.x2 in T.:B1 by A3,FUNCT_2:43;
    hence t in T.:B0+T.:B1 by A4,A5;
    end;
   let t be set;
   assume t in T.:B0 + T.:B1;
   then
   consider tz0,tz1 be Point of Y such that
   P0: t=tz0+tz1 & tz0 in T.:B0 & tz1 in T.:B1;
   consider z0 be Element of the carrier of X such that
   P1: z0 in B0 & tz0=T.z0 by P0,FUNCT_2:116;
   consider z1 be Element of the carrier of X such that
   P2: z1 in B1 & tz1=T.z1 by P0,FUNCT_2:116;
   reconsider z0 as Point of X;
   reconsider z1 as Point of X;
   A2: z0+z1 in B0+B1 by P1,P2;
   t=T.(z0+z1) by LOPBAN_1:def 5,P0,P1,P2;
   hence t in T.:(B0+B1) by A2,FUNCT_2:43;
   end;

theorem Lm032:
  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 set;
     assume t in T.:(a*B0);
     then
     consider z1 be set such that
     A1: z1 in the carrier of X & z1 in a*B0
      & t= T.z1 by FUNCT_2:115;
      consider x1 be Element of X such that
      A3: z1=a*x1 & x1 in B0 by A1;
      A4: t=a* T.x1 by LOPBAN_1:def 6,A1,A3;
      T.x1 in T.:B0 by A3,FUNCT_2:43;
      hence t in a*T.:B0 by A4;
      end;
     let t be set;
      assume t in a*T.:B0;
      then consider tz0 be Point of Y such that
      P0: t=a*tz0 & tz0 in T.:B0;
      consider z0 be Element of the carrier of X such that
      P1: z0 in B0 & tz0=T.z0 by P0,FUNCT_2:116;
      reconsider z0 as Point of X;
      set z1=a*z0;
      A2: z1 in a*B0 by P1;
      t=T. z1 by LOPBAN_1:def 6,P0,P1;
      hence t in T.:(a*B0) by A2,FUNCT_2:43;
      end;

theorem Lm03:
  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 set;
    assume t in T.:(x1+ B0);
     then consider z1 be set such that
    A1: z1 in the carrier of X & z1 in x1+ B0
    & t= T.z1 by FUNCT_2:115;
    reconsider z1 as Point of X by A1;
    consider z0 be Element of X such that
   A3: z1=x1+ z0 & z0 in B0 by A1;
   A4: t=T.x1 + T.z0 by A1,A3,LOPBAN_1:def 5;
   T.z0 in T.:B0 by A3,FUNCT_2:43;
   hence t in T.x1 + T.:B0 by A4;
   end;
   let t be set;
    assume t in T.x1 + T.:B0;
  then consider tz0 be Point of Y such that
  P0: t=T.x1+tz0 & tz0 in T.:B0;
  consider z0 be Element of the carrier of X such that
    P1: z0 in B0 & tz0=T.z0 by P0,FUNCT_2:116;
   A2: x1+z0 in x1+B0 by P1;
    t=T.(x1+z0) by LOPBAN_1:def 5,P0,P1;
     hence t in T.:(x1+ B0) by A2,FUNCT_2:43;
   end;

theorem
  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 & W=W1;
     thus V+W c= V1+W1
     proof
     let x be set;
     assume A3:x in V+W;
     consider u,v be Point of X such that
      A4:x=u+v & u in V & v in W by A3;
     reconsider u1=u as Point of LinearTopSpaceNorm X by A1,A4;
     reconsider v1=v as Point of LinearTopSpaceNorm X by A1,A4;
     u+v=u1+v1 by NORMSP_2:def 4;
     hence x in V1+W1 by A1,A4;
    end;
    let x be set;
     assume B3:x in V1+W1;
     consider u,v be Point of LinearTopSpaceNorm X such that
     B4:x=u+v & u in V1 & v in W1 by B3;
     reconsider u1=u as Point of X by A1,B4;
     reconsider v1=v as Point of X by A1,B4;
     u+v=u1+v1 by NORMSP_2:def 4;
     hence x in V+W by A1,B4;
     end;

theorem Lm05:
  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 & x=x1;
    thus x+V c= x1+V1
    proof
    let z be set;
    assume A3:z in x+V;
    consider u be Point of X such that
    A4:z=x+u & u in V by A3;
    reconsider u1=u as Point of LinearTopSpaceNorm X by A1,A4;
    x+u=x1+u1 by A1,NORMSP_2:def 4;
   hence z in x1+V1 by A1,A4;
   end;
     let z be set;
     assume B3:z in x1+V1;
     consider u1 be Point of LinearTopSpaceNorm X such that
    B4:z=x1+u1 & u1 in V1 by B3;
    reconsider u=u1 as Point of X by A1,B4;
    x1+u1=x+u by A1, NORMSP_2:def 4;
    hence z in x+V by A1,B4;
   end;

theorem Lm06:
  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 set;
    assume A3:z in a*V;
    consider v be Point of X such that
    A4:z=a*v & v in V by A3;
    reconsider v1=v as Point of LinearTopSpaceNorm X by A1,A4;
    a*v=a*v1 by NORMSP_2:def 4;
    hence z in a*V1 by A1,A4;
    end;
    let z be set;
    assume B3:z in a*V1;
    consider v be Point of LinearTopSpaceNorm X such that
    B4:z=a*v & v in V1 by B3;
    reconsider v1=v as Point of X by A1,B4;
    a*v=a*v1 by NORMSP_2:def 4;
    hence z in a*V by A1,B4;
    end;

theorem Lm08:
  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 set;
       assume
       A2: z in Cl(V);
       then z in the carrier of X;
       then
       A21: z in the carrier of LinearTopSpaceNorm X by NORMSP_2:def 4;
      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 A3: D1 is closed;
      assume A31: V1 c= D1;
      reconsider D2=D1 as Subset of TopSpaceNorm X by NORMSP_2:def 4;
       reconsider D0=D1 as Subset of X by NORMSP_2:def 4;
      D0 is closed by NORMSP_2:32,A3;
      then D2 is closed by NORMSP_2:15;
      hence z in D1 by A1,A2,A31,PRE_TOPC:45;
      end;
      hence z in Cl(V1) by A21,PRE_TOPC:45;
    end;
    let z be set;
    assume
    A2: z in Cl(V1);
    then z in the carrier of LinearTopSpaceNorm X;
    then
    A21: z in the carrier of TopSpaceNorm X by NORMSP_2:def 4;
    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 A3: D1 is closed;
      assume A31: V c= D1;
     reconsider D2=D1 as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
     reconsider D0=D1 as Subset of X;
      D0 is closed by NORMSP_2:15,A3;
      then D2 is closed by NORMSP_2:32;
      hence z in D1 by A1,A2,A31,PRE_TOPC:45;
      end;
      hence z in Cl(V) by A21,PRE_TOPC:45;
      end;

theorem Lm10:
  for x be Point of X, r be real number
    holds Ball(0.X,r)=(-1)*Ball(0.X,r)
      proof
      let x be Point of X, r be real number;
     thus Ball(0.X,r) c= (-1)*Ball(0.X,r)
      proof
     let z be set;
   assume
    R1: 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 R1;
   then ||.-z1.|| < r by RLVECT_1:27;
   then ||.-(-z1).|| < r by NORMSP_1:6;
   then ||.0.X-(-z1).|| < r by RLVECT_1:27;
   then R3: -z1 in Ball(0.X,r);
    (-1)*(-z1) =1*z1 by RLVECT_1:40
              .=z1 by RLVECT_1:def 9;
   hence z in (-1)*Ball(0.X,r) by R3;
   end;
  let z be set;
   assume
    R1: z in (-1)*Ball(0.X,r);
   then reconsider z1=z as Point of X;
   consider y1 be Point of X such that
   B1: z1=(-1)* y1 & y1 in Ball(0.X,r) by R1;
    ex zz1 be Point of X st y1 =zz1 & ||.0.X-zz1.||<r by B1;
    then ||.-y1.|| < r by RLVECT_1:27;
   then ||.-(-y1).|| < r by NORMSP_1:6;
   then
   R3:||.0.X-(-y1).|| < r by RLVECT_1:27;
      -y1 =z1 by B1,RLVECT_1:29;
   hence z in Ball(0.X,r) by R3;
   end;

theorem Lm11:
  for x be Point of X,r be real number,
      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 number,
    V be Subset of LinearTopSpaceNorm X;
    assume A1: V = Ball(x,r);
    reconsider V1 = Ball(x,r) as Subset of X;
   K2:for u,v being Point of X, s being 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 A2: 0 < s & s < 1 & u in V1 & v in V1;
            s+0<1 by A2;
       then AX1:1-s >0 by XREAL_1:22;
   A4:  ||.s*x +(1-s)*x -(s*u + (1-s)*v).||
      = ||.s*x  +(-(s*u + (1-s)*v))+(1-s)*x.|| by RLVECT_1:def 6
     .= ||.s*x +(-1)*(s*u + (1-s)*v) +(1-s)*x.|| by RLVECT_1:29
     .= ||.s*x + ((-1)*(s*u) +(-1)*((1-s)*v)) +(1-s)*x.|| by RLVECT_1:def 9
     .= ||.s*x + (-s*u +(-1)*((1-s)*v)) +(1-s)*x.|| by RLVECT_1:29
     .= ||.s*x + (-s*u +-(1-s)*v) + (1-s)*x.|| by RLVECT_1:29
     .= ||.(s*x + -s*u) +-(1-s)*v + (1-s)*x.|| by RLVECT_1:def 6
     .= ||.s*x - s*u + ((1-s)*x -(1-s)*v).|| by RLVECT_1:def 6
     .= ||.s* (x - u) + ((1-s)*x -(1-s)*v).|| by RLVECT_1:48
     .= ||.s* (x - u) + (1-s)*(x -v).|| by RLVECT_1:48;
   A7: 0 < abs(s) by ABSVALUE:def 1,A2;
   A8: 0 < abs(1-s) by ABSVALUE:def 1,AX1;
 AZ1:   ex u1 be Point of X st
      u =u1 & ||.x-u1.||<r by A2;
    ex v1 be Point of X st v =v1 & ||.x-v1.||<r by A2; then
      abs(s)*||.x-u.|| < abs(s)*r &
   abs(1-s)*||.x-v.|| < abs(1-s)*r by A7,A8,XREAL_1:70,AZ1; then
   abs(s)*||.x-u.|| + abs(1-s)*||.x-v.|| <
                   abs(s)*r + abs(1-s)*r by XREAL_1:10;
     then abs(s)*||.x-u.|| + abs(1-s)*||.x-v.|| <
                    s*r + abs(1-s)*r by A2,ABSVALUE:def 1;
      then abs(s)*||.x-u.|| + abs(1-s)*||.x-v.|| <
                    s*r + (1-s)*r by AX1,ABSVALUE:def 1;
     then ||.s*(x-u).|| + abs(1-s)*||.x-v.|| < 1* r by NORMSP_1:def 2;
     then
   A9:||.s*(x-u).|| + ||.(1-s)*(x-v).|| < r by NORMSP_1:def 2;
     ||.s*x +(1-s)*x -(s*u + (1-s)*v).|| <=
          ||.s*(x-u).|| + ||.(1-s)*(x-v).|| by A4,NORMSP_1:def 2;
     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 9;
      then ||.x -(s*u + (1-s)*v).|| < r by RLVECT_1:def 9;
    hence thesis;
   end;
   for u,v being Point of LinearTopSpaceNorm X,
   s being Real st 0 < s & s < 1 & u in V & v in V
   holds s*u + (1-s)*v in V
   proof
   let u,v being Point of LinearTopSpaceNorm X;
   let s being Real;
   assume ASV: 0 < s & s < 1 & u in V & v in V;
   reconsider u1=u as Point of X by NORMSP_2:def 4;
   reconsider v1=v as Point of X by NORMSP_2:def 4;
   L2: s*u1 = s*u by NORMSP_2:def 4;
   L3: (1-s)*v1 =(1-s)*v by NORMSP_2:def 4;
   s*u1 + (1-s)*v1 = s*u + (1-s)*v by NORMSP_2:def 4,L2,L3;
   hence thesis by A1,K2,ASV;
   end;
   hence thesis by CONVEX1:def 2;
   end;

theorem Lm12:
  for x be Point of X,r be real number,
    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 number,
   T be LinearOperator of X,Y,
   V be Subset of LinearTopSpaceNorm Y;
   assume A1: V = T.: Ball(x,r);
   reconsider V1 = T.: Ball(x,r) as Subset of Y;
    K2:for u,v being Point of Y, s being Real
      st 0 < s & s <1 & u in V1 & v in V1 holds s*u + (1-s)*v in V1
  proof
  let u,v being Point of Y,
   s being Real;
   assume A2: 0 < s & s < 1 & u in V1 & v in V1;
       consider z1 be set such that
      A3: z1 in the carrier of X & z1 in Ball(x,r)
       & u= T.z1 by A2,FUNCT_2:115;
    reconsider zz1=z1 as Point of X by A3;
    A6:  s*u=T.(s*zz1) by LOPBAN_1:def 6,A3;
    consider z2 be set such that
      A7: z2 in the carrier of X & z2 in Ball(x,r)
       & v= T.z2 by A2,FUNCT_2:115;
    reconsider zz2=z2 as Point of X by A7;
    A10:  (1-s)*v=T.((1-s)*zz2) by LOPBAN_1:def 6,A7;
     reconsider za1=zz1 as Point of LinearTopSpaceNorm X by NORMSP_2:def 4;
     reconsider za2=zz2 as Point of LinearTopSpaceNorm X by NORMSP_2:def 4;
     reconsider Bxr =Ball(x,r) as Subset of
                         LinearTopSpaceNorm X by NORMSP_2:def 4;
       Bxr is convex by Lm11; then
      AM1:s*za1 + (1-s)*za2 in Bxr by A2,A3,A7,CONVEX1:def 2;
      AM2: s*za1 =s*zz1 by NORMSP_2:def 4;
      AM3: (1-s)*za2 =(1-s)*zz2 by NORMSP_2:def 4;
      AM4:  s*za1 + (1-s)*za2=s*zz1 + (1-s)*zz2 by NORMSP_2:def 4,AM2,AM3;
           s*u + (1-s)*v =T.(s*zz1 + (1-s)*zz2) by LOPBAN_1:def 5,A6,A10;
    hence thesis by FUNCT_2:43,AM1,AM4;
   end;
   for u,v being Point of LinearTopSpaceNorm Y,
   s being Real st 0 < s & s < 1 & u in V & v in V
   holds s*u + (1-s)*v in V
   proof
   let u,v being Point of LinearTopSpaceNorm Y;
   let s be Real;
   assume ASV: 0 < s & s < 1 & u in V & v in V;
   reconsider u1=u as Point of Y by NORMSP_2:def 4;
   reconsider v1=v as Point of Y by NORMSP_2:def 4;
   L2: s*u1 =s*u by NORMSP_2:def 4;
   L3: (1-s)*v1 =(1-s)*v by NORMSP_2:def 4;
   s*u1 + (1-s)*v1 =s*u + (1-s)*v by NORMSP_2:def 4,L2,L3;
   hence thesis by K2,A1,ASV;
  end;
  hence thesis by CONVEX1:def 2;
   end;

theorem Lm13:
  for x be Point of X, r, s be real number st r <= s
  holds Ball(x,r) c= Ball(x,s)
  proof
  let x be Point of X, r, s be real number;
  assume
  A1:  r <=s;
  for u being Point of X st u in Ball(x,r) holds u in Ball(x,s)
  proof
    let u be Point of X;
    assume A2:u in Ball(x,r);
   ex uu1 be Point of X st u=uu1 & ||.x-uu1.|| < r by A2;
    then ||.x-u.|| + r < r + s by A1,XREAL_1:10;
    then ||.x-u.|| < r + s - r by XREAL_1:22;
    hence thesis;
  end;
  hence thesis by SUBSET_1:7;
end;

:: Open Mapping lemma

theorem LM040:
  for X be RealBanachSpace, Y be RealNormSpace,
    T be bounded LinearOperator of X,Y,
    r be real number,
    BX1 be Subset of LinearTopSpaceNorm X,
    TBX1,BYr be Subset of LinearTopSpaceNorm Y
  st r>0 & BX1=Ball(0.X,1) & 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 bounded LinearOperator of X,Y,
     r be real number,
    BX1  be Subset of LinearTopSpaceNorm X,
    TBX1,BYr  be Subset of LinearTopSpaceNorm Y;
assume
AS0: r>0 & BX1=Ball(0.X,1) & BYr=Ball(0.Y,r )
    & TBX1=T.: Ball(0.X,1) & BYr c= Cl (TBX1);
A1: for x be Point of X,y be Point of Y,
        TB1, BYsr be Subset of LinearTopSpaceNorm Y,
        s be real number
        st s >0 & TB1=T.: Ball(x,s) & y=T.x
        & BYsr =Ball(y,s*r)
        holds BYsr c= Cl (TB1)
     proof
    let x be Point of X, y be Point of Y,
    TB1, BYsr be Subset of LinearTopSpaceNorm Y,
     s be real number;
     assume
   A2: s >0 & TB1=T.: Ball(x,s) & y=T.x & BYsr =Ball(y,s*r);
    reconsider TB0 = T.:Ball(0.X,s)
       as Subset of LinearTopSpaceNorm Y by NORMSP_2:def 4;
    reconsider x1=x as Point of LinearTopSpaceNorm X by NORMSP_2:def 4;
    reconsider y1=y as Point of LinearTopSpaceNorm Y by NORMSP_2:def 4;
    reconsider s1 = s as non zero Real by A2,XREAL_0:def 1;
                   s1*BYr c= s1*Cl (TBX1) by AS0,CONVEX1:39;
    then s1*BYr c= Cl (s1*TBX1) by RLTOPSP1:53;
    then y1+s1*BYr c= y1+Cl (s1*TBX1) by RLTOPSP1:8;
    then
    P1: y1+s1*BYr c= Cl (y1+s1*TBX1) by RLTOPSP1:39;
    Q1: Ball(y,s*r) =y + Ball(0.Y,s*r) by Lm01;
    Ball(0.Y,s*r)=s1*Ball(0.Y,r) by A2,Lm02; then
    Ball(0.Y,s*r)  = s1*BYr by Lm06,AS0; then
    P2: y1+s1*BYr=BYsr by A2,Q1,Lm05;
    reconsider TB0s = T.: Ball(0.X,s) as Subset of Y;
    reconsider TB01 = T.: Ball(0.X,1) as Subset of Y;
    reconsider TB0xs = T.: Ball(x,s) as Subset of Y;
   Ball(x,s) = x+Ball(0.X,s) by Lm01; then
   Q3: y+TB0s = TB0xs by A2,Lm03;
   Q4:s1*TB01 =s1* TBX1 by AS0,Lm06;
    s1*Ball(0.X,1)= Ball(0.X,s1*1) by A2,Lm02;
   hence thesis by P1,P2,Q3,A2,Lm05,Q4,Lm032;
   end;
  B1: for s0 be real number st s0 >0 holds
      Ball(0.Y,r ) c= T.: Ball(0.X,1+s0)
      proof
     let s0 be real number;
    assume C1:s0 >0;
    now let z be set;
    assume
    C2: z in Ball(0.Y,r); then
    reconsider y =z as Point of Y;
    consider s1 be real number such that
    C21: 0 < s1 & s1 < s0 by C1,XREAL_1:7;
    set a=s1/(1+s1);
    set e= a GeoSeq;
    C23:0<a by C21,XREAL_1:141;
    C24: a<1 by C21,XREAL_1:193,XREAL_1:31; then
     abs(a) < 1 by C21,ABSVALUE:def 1; then
   C3: e is summable & Sum(e) = 1/(1-a) by SERIES_1:28;
   C4: Sum(e) < 1+s0
        proof
          1/(1-a)=1/((1*(1+s1)-s1)/(1+s1)) by C21,XCMPLX_1:128
                .=1+s1 by XCMPLX_1:101;
         hence thesis by C3,C21,XREAL_1:8;
        end;
    C5: e.0 = 1 by PREPOWER:4;
           reconsider B0 =Ball(y,e.1*r) as Subset of
                         LinearTopSpaceNorm Y by NORMSP_2:def 4;
           A13: B0 is open by NORMSP_2:23;
            CK1: e.1=a|^1 by PREPOWER:def 1;
            CK2: 0<a|^1 by C23,NEWTON:102;
            CK3:0< e.1*r by CK1,CK2,AS0,XREAL_1:131;
           ||.y-y.|| < e.1*r by CK3,NORMSP_1:10; then
           A14: y in B0;
           Ball(y,e.1*r) meets TBX1 by AS0,C2,A13,A14,PRE_TOPC:def 13;
          then
          consider s be set such that
          C600: s in Ball(y,e.1*r) & s in T.: Ball(0.X,1)
            by AS0,XBOOLE_0:3;
            consider xn1 be set such that
          C601: xn1 in the carrier of X & xn1 in Ball(0.X,1) & s = T.xn1
           by C600,FUNCT_2:115;
            reconsider xn1 as Point of X by C601;
           reconsider sb=T.xn1 as Point of Y;
       CS1: ex ss1  be Point of Y st
          sb=ss1 & ||.y-ss1.|| < e.1*r by C600,C601;
   defpred P[Element of 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;
    C6:   for n being Element of NAT for v,w be Point of X
         ex z being Point of X st P[n,v,w,z]
     proof
      let n being Element of NAT;
      let v,w be Point of X;
       now
         assume CAS1:w in Ball(v,e.n) & ||.T.w-y.|| < e.(n+1)*r;
         CX1: e.(n+1)=a|^(n+1) by PREPOWER:def 1;
          reconsider TB1 = T.: Ball(w,e.(n+1)) 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;
           A12: BYsr c= Cl (TB1) by CX1,C23,NEWTON:102,A1;
           reconsider B0 = Ball(y,e.(n+2)*r) as Subset of
                         LinearTopSpaceNorm Y by NORMSP_2:def 4;
           A13: B0 is open by NORMSP_2:23;
            CK1: e.(n+2)=a|^(n+2) by PREPOWER:def 1;
            CK2: 0<a|^(n+2) by C23,NEWTON:102;
                 0< e.(n+2)*r by CK1,CK2,AS0,XREAL_1:131;
             then ||.y-y.|| < e.(n+2)*r by NORMSP_1:10;
           then
           A14: y in B0;
           y in BYsr by CAS1; then
            Ball(y,e.(n+2)*r) meets TB1 by A12,A13,A14,PRE_TOPC:def 13;
          then consider s be set such that
          C61: s in Ball(y,e.(n+2)*r) & s in T.: Ball(w,e.(n+1))
            by XBOOLE_0:3;
            consider z be set such that
           C62: z in the carrier of X & z in Ball(w,e.(n+1)) & s = T.z
           by C61,FUNCT_2:115;
            reconsider z as Point of X by C62;
            reconsider sb=T.z as Point of Y;
          ex ss1 be Point of Y st
          sb=ss1 & ||.y-ss1.|| < e.(n+2)*r by C61,C62; then
            z in Ball(w,e.(n+1)) & ||.T.z-y.|| < e.(n+2)*r
                                 by C62,NORMSP_1:11;
           hence ex z be Point of X st
          z in Ball(w,e.(n+1)) & ||.T.z-y.|| < e.(n+2)*r;
        end;
      hence thesis;
    end;
    consider xn be sequence of X such that
    C7:  xn.0 = 0.X & xn.1 = xn1
    & for n being Element of NAT
    holds P[n,xn.n,xn.(n+1),xn.(n+2)] from RecExD3(C6);
    C70: for n be Element of NAT holds
            xn.(n+1) in Ball(xn.n,e.n) &
               ||.T.(xn.(n+1))-y.|| < e.(n+1)*r
      proof
      defpred PN[Element of NAT] means
            xn.($1+1) in Ball(xn.$1,e.$1) &
               ||.T.(xn.($1+1))-y.|| < e.($1+1)*r;
       CG1:PN[0] by CS1,C601,PREPOWER:4,NORMSP_1:11,C7;
       CG2:now let n be Element of NAT;
          assume
       CH1:PN[n];
           P[n,xn.n,xn.(n+1),xn.(n+2)] by C7;
           hence PN[n+1] by CH1;
           end;
         thus for n be Element of NAT holds PN[n] from NAT_1:sch 1(CG1,CG2);
      end;
     C800: for m, k be Element of NAT
    holds ||.xn.(m+k) - xn.m.|| <= e.m*((1-e.k)/(1-e.1))
   proof
   let m be Element of NAT;
   defpred PN[Element of NAT] means
     ||.xn.(m+$1) - xn.m.|| <= e.m*((1-e.$1)/(1-e.1));
     PP0: PN[ 0]
     proof
        ||.xn.(m+0) - xn.m.|| = ||.0.X.|| by RLVECT_1:16;
       hence ||.xn.(m+0) - xn.m.|| <=e.m*((1-e.0)/(1-e.1)) by C5;
       end;
       PP1: now let k be Element of NAT;
          assume PP11: PN[k];
       PP13:  ||.xn.((m+k)+1) - xn.m.||
    <= ||.xn.((m+k)+1) - xn.(m+k).|| + ||.xn.(m+k) - xn.m.|| by NORMSP_1:14;
         ||.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 PP11,XREAL_1:8; then
          PP15: ||.xn.(m+(k+1)) - xn.m.||
               <= ||.xn.((m+k)+1) - xn.(m+k).|| + e.m*((1-e.k)/(1-e.1))
                                                by PP13,XXREAL_0:2;
          PB1: xn.(m+k+1) in Ball(xn.(m+k),e.(m+k)) by C70;
          ex xn2 be Point of X st
            xn.((m+k)+1)=xn2 & ||.xn.(m+k) - xn2.||< e.(m+k) by PB1;
            then
         PB2: ||.xn.((m+k)+1) - xn.(m+k).|| < e.(m+k) by NORMSP_1:11;
         PP16: ||.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 PB2, XREAL_1:8;
                 a|^1<1 by C24,NEWTON:10;
                 then 0< 1-a|^1 by XREAL_1:52; then
             MB6:a|^k=((a|^k)*(1-a|^1))/(1-a|^1) by XCMPLX_1:90
                    .=(a|^k-a|^k*a|^1)/(1-a|^1)
                    .=(a|^k-a|^(k+1))/(1-a|^1) by NEWTON:13;
             MB7:(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:63
                .=(1-a|^(k+1))/(1-a|^1);
            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:13
            .=a|^m*((1-a|^(k+1))/(1-a|^1)) by MB6,MB7
            .=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 PP16, PP15,XXREAL_0:2;
        end;
       for k be Element of NAT holds PN[ k] from NAT_1:sch 1(PP0,PP1);
         hence thesis;
       end;
     A39: now let m be Element of NAT;
     hereby let k be Element of NAT;
    A40: ||.xn.(m+k)-xn.m.|| <= e.m*((1-e.k)/(1-e.1)) by C800;
    A41:0 < a|^m & 0 < a|^k & 0 < a|^1 by NEWTON:102,C23;
         AL1:1-a|^k < 1 by XREAL_1:46,NEWTON:102,C23;
                a|^1 < 1 by C24,NEWTON:10; then
         AL22: 0< 1-a|^1 by XREAL_1:52;
          (1-a|^k)/(1-a|^1)< 1/(1-a|^1) by AL1,AL22, XREAL_1:76; then
         AL23: a|^m*((1-a|^k)/(1-a|^1)) < a|^m*(1/(1-a|^1))
                                      by A41,XREAL_1:70;
         ||.xn.(m+k)-xn.m.|| <= a|^m*((1-e.k)/(1-e.1)) by PREPOWER:def 1,A40;
           then
         ||.xn.(m+k)-xn.m.|| <= a|^m*((1-a|^k)/(1-e.1)) by PREPOWER:def 1;
            then
         ||.xn.(m+k)-xn.m.|| <= a|^m*((1-a|^k)/(1-a|^1)) by PREPOWER:def 1;
         hence ||.xn.(m+k)-xn.m.|| < a|^m*(1/(1-a|^1)) by AL23,XXREAL_0:2;
     end;
    end;
     now let r1 be Real;
     assume AP1:0 < r1;
          a|^1 < 1 by C24,NEWTON:10; then
         AF1:0< 1-a|^1 by XREAL_1:52;
         AP2:0< r1*(1-a|^1) by AP1,AF1,XREAL_1:131;
       KK1: e is convergent & lim e =0 by C3,SERIES_1:7;
             consider p1 be Element of NAT such that
       KK2:    for m be Element of NAT
                 st p1<=m holds abs(e.m-0)< r1*(1-a|^1)
                       by AP2,SEQ_2:def 7,KK1;
                abs(e.p1-0)< r1*(1-a|^1) by KK2; 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 AF1,XREAL_1:76; then
                e.p1/(1-a|^1) < r1 by AF1,XCMPLX_1:90; then
                a|^p1/(1-a|^1) < r1 by PREPOWER:def 1; then
            A42:a|^p1*(1/(1-a|^1)) < r1 by XCMPLX_1:100;
          take m=p1;
          hereby let n be Element of NAT;
          assume m <= n;
          then consider k1 be Nat such that
       A44:   n = m + k1 by NAT_1:10;
      reconsider k1 as Element of NAT by ORDINAL1:def 13;
      n = m + k1 by A44;
      hence ||.xn.n-xn.m.|| < r1 by A39,A42,XXREAL_0:2;
     end;
    end;
     then xn is Cauchy_sequence_by_Norm by LOPBAN_3:5; then
     C9: xn is convergent by LOPBAN_1:def 16;
     set xx= lim xn;
    C91: ||.xn.|| is convergent & lim ||.xn.|| = ||.lim xn.||
             by C9,LOPBAN_1:47;
     for k be Element of NAT st 0 <= k holds
     ||.xn.||.k <= 1/(1-a)
     proof
    let k be Element of NAT;
    assume 0 <= k;
     ||. xn.(0+k) - xn.0 .|| <= e.0*((1-e.k)/(1-e.1)) by C800;
    then
    F1: ||.xn.k .|| <= (1-e.k)/(1-e.1) by C5,C7,RLVECT_1:26;
    F2:e.k = a|^k by PREPOWER:def 1;
    F21:e.1 = a|^1 by PREPOWER:def 1;
    F5:1-a|^k <1 by NEWTON:102,C23,XREAL_1:46;
       a|^1 < 1 by C24,NEWTON:10;
       then
       0< 1-a|^1 by XREAL_1:52;
       then
       (1-e.k)/(1-e.1) <= 1/(1-a|^1) by F2,F21,F5,XREAL_1:76;
       then (1-e.k)/(1-e.1) <= 1/(1-a ) by NEWTON:10;
       then ||.xn.k .|| <= 1/(1-a ) by F1,XXREAL_0:2;
       hence thesis by NORMSP_1:def 10;
       end;
       then ||.xx .|| <= Sum(e) by C3,C91,RSSPACE2:6;
       then ||.xx.|| < 1+s0 by C4,XXREAL_0:2;
       then ||.-xx.|| < 1+s0 by NORMSP_1:6;
       then ||.0.X-xx.|| < 1+s0 by RLVECT_1:27;
       then
     C11: xx in Ball(0.X,1+s0);
       rng xn c= the carrier of X; then
       C1200: rng xn c= dom T by FUNCT_2:def 1;
              T is_continuous_in xx by LOPBAN_5:4; then
       C1220: T/*xn is convergent & T/.xx = lim (T/*xn)
       by C1200,NFCONT_1:def 9,C9;
     C123: now let n be Element of NAT;
        thus (T/*xn).n=T/.(xn.n) by C1200,FUNCT_2:186
                    .=T.(xn.n);
      end;
      now let s be Real;
      assume A1: 0 < s;
             A2:0< s/r by AS0,A1,XREAL_1:141;
       KK1: e is convergent & lim e =0 by C3,SERIES_1:7;
              consider m0 be Element of NAT such that
       KK2: for n be  Element of NAT
               st m0<=n holds abs(e.n-0)< s/r by A2,SEQ_2:def 7,KK1;
            abs(e.m0-0)< s/r by KK2; then
           KK4: e.m0 < 0+s/r by RINFSUP1:1;
             MB6: 0< a|^1 & a|^1 < 1 by C23,C24,NEWTON:10;
             0 < a|^m0 by NEWTON:102,C23; then
             a|^m0*a|^1 <= a|^m0 by MB6,XREAL_1:155;
             then a|^(m0+1) <= a|^m0 by NEWTON:13;
             then e.(m0+1) <= a|^m0 by PREPOWER:def 1;
             then e.(m0+1) <= e.m0 by PREPOWER:def 1;
             then e.(m0+1)< s/r by KK4,XXREAL_0:2;
             then e.(m0+1)*r < s/r*r by AS0,XREAL_1:70;
             then
             A2:e.(m0+1)*r < s by AS0,XCMPLX_1:88;
        take m=m0+1;
      now let n be Element of NAT;
      assume
      A3: m <= n;
    1 <= m0+1 by NAT_1:11; then
    reconsider n0= n-1 as Element of NAT by NAT_1:21,A3,XXREAL_0:2;
    consider m1 be Nat such that
     AB1: n0+1 = m0+1 + m1 by A3,NAT_1:10;
      AB2: a |^(n0+1) = a |^(m0+1) * a |^ m1 by AB1,NEWTON:13;
      AB3: 0< a |^(m0+1) & 0< a |^ m1 by NEWTON:102,C23;
     AL1: a|^m1 <= 1|^m1 by PREPOWER:17,C23,C24;
           1|^m1=1 by NEWTON:15; then
         a |^(n0+1) <= a |^(m0+1) by AB2,AB3,AL1,REAL_2:147;
     then e.(n0+1) <= a |^(m0+1) by PREPOWER:def 1;
     then e.(n0+1) <= e.(m0+1) by PREPOWER:def 1; then
      A5: e.(n0+1)*r <= e.(m0+1)*r by AS0,XREAL_1:66;
        ||.T.(xn.n)-y.|| <= e.(m0+1)*r by A5,XXREAL_0:2,C70; then
        ||.T.(xn.n)-y.|| < s by A2,XXREAL_0:2;
       hence ||.(T/*xn).n-y.|| < s by C123;
     end;
    hence for n be Element of NAT st m <= n holds ||.(T/*xn).n-y.|| < s;
   end;
    then y=T.xx by NORMSP_1:def 11,C1220;
    hence z in T.:Ball(0.X,1+s0) by C11, FUNCT_2:43;
    end;
   hence thesis by TARSKI:def 3;
   end;
   now let z be set;
    assume
   R1: 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 R1;
    then ||.-y.|| < r by RLVECT_1:27; then
  R2:||.y.|| < r by NORMSP_1:6;
     RX1:0<=||.y.|| by NORMSP_1:8;
   consider s0 be real number such that
   RX2: 0<s0 & ||.y.||< r/(1+s0) & r/(1+s0) < r by R2,RX1,Lm00;
         (1+s0)*||.y.|| < r/(1+s0)*(1+s0) by RX2,XREAL_1:70;
        then (1+s0)*||.y.|| < r by RX2,XCMPLX_1:88;
        then abs(1+s0)*||.y.|| < r by RX2,ABSVALUE:def 1;
        then
      R3:||.(1+s0)*y.|| < r by NORMSP_1:def 2;
       set y1=(1+s0)*y;
        ||.-y1.|| < r by NORMSP_1:6,R3;
        then ||.0.Y-y1.|| < r by RLVECT_1:27;
        then
       R4:(1+s0)*y in Ball(0.Y,r);
        Ball(0.Y,r) c= T.: Ball(0.X,1+s0) by B1,RX2;
         then
       R5:(1+s0)*y in T.: Ball(0.X,1+s0) by R4;
      reconsider s1=1+s0 as non zero Real by RX2;
      reconsider TB0s = T.: Ball(0.X,s1) as Subset of Y;
     reconsider TB01 = T.: Ball(0.X,1) as Subset of Y;
     s1*Ball(0.X,1)= Ball(0.X,s1*1) by RX2,Lm02;
     then s1*y in s1*TB01 by R5,Lm032;
      then s1"*(s1*y) in s1"*(s1*TB01);
      then (s1"*s1)*y in s1"*(s1*TB01) by RLVECT_1:def 9;
      then
    LN1:(s1"*s1)*y in (s1"*s1)*TB01 by CONVEX1:37;
         s1"*s1=(1/s1)*s1 by XCMPLX_1:217
              .=1 by XCMPLX_1:107;
      then y in 1*TB01 by LN1,RLVECT_1:def 9;
       hence z in T.: Ball(0.X,1) by CONVEX1:32;
     end;
   hence thesis by AS0,TARSKI:def 3;
end;

:: Open Mapping Theorem

theorem
  for X, Y be RealBanachSpace,
    T be bounded 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 bounded LinearOperator of X,Y,
    T1 be Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y;
    assume AS0: T1=T & T1 is onto;
   thus for G be Subset of LinearTopSpaceNorm X st
     G is open holds T1.:G is open
    proof
      let G be Subset of LinearTopSpaceNorm X;
      assume AA1: G is open;
  defpred P[Element of NAT, set]
   means ex TBn be Subset of TopSpaceNorm Y
    st TBn=T.: Ball(0.X,$1) & $2=Cl(TBn);
P1: for n being Element of NAT ex y being Element of bool the carrier of Y
     st P[n,y]
    proof
    let n being 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 Function of NAT,bool (the carrier of Y) such that
   P2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(P1);
    reconsider f as SetSequence of Y;
     AD1: union rng f is Subset of Y by PROB_1:23;
    the carrier of Y c= union rng f
    proof
      let z be set;
      assume z in the carrier of Y;
      then reconsider z1=z as Point of Y;
  AQ1:rng T = the carrier of (LinearTopSpaceNorm Y ) by AS0,FUNCT_2:def 3;
      rng T = the carrier of Y by AQ1,NORMSP_2:def 4; then
      consider x1 be set such that
 AZ3: x1 in the carrier of X & z1=T.x1 by FUNCT_2:17;
      reconsider x1 as Point of X by AZ3;
      consider m be Element of NAT such that
 AZ9: ||.x1.|| <= m by MESFUNC1:11;
      set n=m+1;
      ||.x1.|| +0< m+1 by XREAL_1:10,AZ9;
      then ||.-x1.|| < n by NORMSP_1:6;
      then ||.0.X-x1.|| < n by RLVECT_1:27; then
 AZ4: x1 in Ball(0.X,n);
 AZ7: T.x1 in T.:Ball(0.X,n) by FUNCT_2:43,AZ4;
      consider TBn be Subset of TopSpaceNorm Y such that
 AZ5: TBn=T.: Ball(0.X,n) & f.n =Cl(TBn) by P2;
AZ6:  TBn c= f.n by PRE_TOPC:48,AZ5;
      NAT=dom f by FUNCT_2:def 1;
      then
     f.n in rng f by FUNCT_1:12;
     hence z in union rng f by AZ3,AZ5,AZ6,AZ7,TARSKI:def 4;
    end; then
   P3:union rng f = the carrier of Y by AD1,XBOOLE_0:def 10;
     for n be Element of NAT holds f.n is closed
     proof
      let n be Element of NAT;
      consider TBn be Subset of TopSpaceNorm Y such that
     P31: TBn=T.: Ball(0.X,n) & f.n=Cl(TBn) by P2;
        thus f.n is closed by NORMSP_2:15,P31;
       end;
      then
      consider n0 be Element of NAT, r be Real, y0 be Point of Y such that
  P4: 0 < r & Ball (y0,r) c= f.n0 by LOPBAN_5:3,P3;
         consider TBn0 be Subset of TopSpaceNorm Y such that
       YP0: TBn0=T.: Ball(0.X,n0) & f.n0=Cl(TBn0) by P2;
        consider TBn01 be Subset of TopSpaceNorm Y such that
       YP1: TBn01=T.: Ball(0.X,n0+1) & f.(n0+1)=Cl(TBn01) by P2;
        Ball(0.X,n0) c= Ball(0.X,n0+1) by NAT_1:11,Lm13;
        then TBn0 c= TBn01 by YP0,YP1,RELAT_1:156;
        then f.n0 c= f.(n0+1) by PRE_TOPC:49,YP0,YP1; then
         YP3:Ball (y0,r) c= Cl(TBn01) by YP1,P4, XBOOLE_1:1;
         ||.y0-y0.|| < r by P4,NORMSP_1:10;
       then y0 in Ball (y0,r); then
      ZP4: y0 in Cl(TBn01) by YP3;
      reconsider LTBn01=TBn01 as Subset of LinearTopSpaceNorm(Y)
                   by NORMSP_2:def 4;
       (-1) is non zero Real; then
       ZP5: Cl((-1)*LTBn01) =(-1)*Cl(LTBn01) by RLTOPSP1:53;
     reconsider XB01 = Ball(0.X,n0+1) as Subset of X;
     reconsider XTB01 = T.: Ball(0.X,n0+1) as Subset of Y;
       ZP6: (-1)*LTBn01 = (-1)* (XTB01) by Lm06,YP1
                       .= T.:((-1)*Ball(0.X,n0+1)) by Lm032
                       .= LTBn01 by YP1,Lm10;
     reconsider yy0 = y0 as Point of LinearTopSpaceNorm Y
              by NORMSP_2:def 4;
    YY1: -yy0=(-1)*yy0 by RLVECT_1:29
            .=(-1)*y0 by NORMSP_2:def 4
            .=-y0 by RLVECT_1:29;
      reconsider BYr = Ball(0.Y,r) 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;
        yy0 in Cl(LTBn01) by Lm08,ZP4;
        then (-1)*yy0 in (-1)*Cl(LTBn01); then
        -yy0 in Cl(LTBn01) by ZP5,ZP6,RLVECT_1:29; then
        YP4: -yy0 in Cl(TBn01) by Lm08;
        Ball (y0,r) = y0 + Ball (0.Y,r) by Lm01;
        then BYyr = yy0+ BYr by Lm05;
        then (-yy0)+BYyr =(-yy0 + yy0)+ BYr by RLTOPSP1:6;
        then (-yy0)+BYyr =0.(LinearTopSpaceNorm Y)+ BYr by RLVECT_1:16;
        then (-yy0)+BYyr ={0.(LinearTopSpaceNorm Y)}+ BYr by RUSUB_4:36;
        then (-yy0)+BYyr = BYr by CONVEX1:35;
        then
         YP5: Ball (0.Y,r) = -y0 + Ball (y0,r) by Lm05,YY1;
      reconsider TBnx01 = T.: Ball(0.X,n0+1) as Subset of LinearTopSpaceNorm Y
                                  by NORMSP_2:def 4;
      reconsider my0 = {-yy0} as Subset of LinearTopSpaceNorm Y;
       YP11: BYyr c= Cl(TBnx01) by Lm08,YP3,YP1;
           {-yy0} c= Cl(TBn01) by YP4,ZFMISC_1:37;
       then my0 c= Cl(TBnx01) by Lm08,YP1;
       then my0 + BYyr c= Cl(TBnx01) + Cl(TBnx01) by YP11,RLTOPSP1:11;
       then
       -yy0 + BYyr c= Cl(TBnx01) + Cl(TBnx01) by RUSUB_4:36;
       then
        YP6: -y0 + Ball (y0,r) c= Cl(TBnx01) + Cl(TBnx01) by YY1,Lm05;
       Cl(TBnx01) + Cl(TBnx01) c= Cl(TBnx01+TBnx01) by RLTOPSP1:63;
          then
         YP7: Ball (0.Y,r) c= Cl(TBnx01+TBnx01) by YP5,YP6,XBOOLE_1:1;
         YP71: TBnx01= 1* TBnx01 by CONVEX1:32;
      reconsider TB1 = T.: Ball(0.X,1) as Subset of LinearTopSpaceNorm Y
                                  by NORMSP_2:def 4;
           YP8:TBnx01+TBnx01 =(1+1)* TBnx01 by YP71, Lm12,CONVEX1:13
                            .= 2 * TBnx01;
       reconsider TBX1 = T.: Ball(0.X,1) as Subset of Y;
           Ball(0.X,(n0+1)*1) = (n0+1) * Ball(0.X,1) by Lm02;
          then (n0+1)*TBX1 = T.: Ball(0.X,n0+1) by Lm032;
          then TBnx01+TBnx01 = 2* ((n0+1)*TB1) by YP8,Lm06
                         .= (2*(n0+1))*TB1 by CONVEX1:37
                         .=(2*n0+2)*TB1;
         then
         YP10: Cl(TBnx01+TBnx01) = (2*n0+2)* Cl(TB1) by RLTOPSP1:53;
         YP13: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:107
                           .= Cl(TB1) by CONVEX1:32;
 reconsider nb1 =1/(2*n0+2) as non zero Real by XREAL_1:141;
     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:75
   .=nb1 * Ball(0.Y,r) by Lm02
   .= nb1 * BYr by Lm06; then
   Q4:Ball (0.Y, r/(2*n0+2)) c= 1/(2*n0+2) *((2*n0+2)* Cl(TB1))
                                      by YP10,YP7, CONVEX1:39;
   Q5: 0 < r/(2*n0+2) by XREAL_1:141,P4;
      Ball(0.X,1) is Subset of LinearTopSpaceNorm X &
      Ball (0.Y,r/(2*n0+2)) is Subset of LinearTopSpaceNorm Y
                                by NORMSP_2:def 4; then
   P5:Ball (0.Y,r/(2*n0+2)) c= T.: Ball(0.X,1)
                              by LM040,Q4,XREAL_1:141,P4,YP13;
   P6: for p be Real st p > 0 ex q be Real st
      0 < q & Ball (0.Y,q) c=T.: Ball(0.X,p)
      proof
      let p be Real;
        assume P61: p > 0;
      reconsider TB1 =T.: Ball(0.X,1) as Subset of Y;
      P610:p*Ball(0.X,1)= Ball(0.X,p*1) by P61,Lm02;
           p* Ball (0.Y,r/(2*n0+2)) c= p*TB1 by P5,CONVEX1:39; then
      P612:  Ball (0.Y,r/(2*n0+2)*p) c= p*TB1 by P61,Lm02;
      take q=r/(2*n0+2)*p;
     thus thesis by P61,P610,P612,Lm032,Q5,XREAL_1:131;
    end;
  now let y be Point of Y;
  assume P7: y in T1.:G;
  consider x be Point of X such that
  P8: x in G & y=T.x by P7,AS0,FUNCT_2:116;
   consider p be Real such that
   P9: p>0 & {z where z is Point of X: ||.x-z.|| < p} c= G
   by NORMSP_2:22,P8,AA1;
   Ball(x,p) c= G by P9; then
   P11: x+Ball(0.X,p) c= G by Lm01;
  reconsider TBp =T.: Ball(0.X,p) as Subset of Y;
   now let t be set;
  assume t in y + TBp; then
  consider tz0 be Point of Y such that
  AB0: t=y+tz0 & tz0 in TBp;
  consider z0 be Element of the carrier of X such that
  AB1: z0 in Ball(0.X,p) & tz0=T.z0 by AB0,FUNCT_2:116;
  reconsider z0 as Point of X;
 A2: x+ z0 in x+Ball(0.X,p) by AB1;
  t=T.(x+z0) by AB0,AB1,P8,LOPBAN_1:def 5;
   hence t in T1.:G by A2,P11,AS0,FUNCT_2:43;
   end; then
  Q11: y + TBp c= T.: G by AS0,TARSKI:def 3;
  consider q be Real such that
  P12: 0 < q & Ball (0.Y,q) c=TBp by P6,P9;
  take q;
  now let t be set;
  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 P12;
 end;
 then y + Ball (0.Y,q) c= y+ TBp by TARSKI:def 3;
  then Ball (y,q) c= y+ TBp by Lm01;
  hence 0 < q & {w where w is Point of Y: ||.y-w.|| < q } c= T1.:G
                                 by AS0,Q11,XBOOLE_1:1,P12;
  end;
hence T1.:G is open by NORMSP_2:22;
end;
end;