let X, Y be RealBanachSpace; :: thesis: for T being Lipschitzian LinearOperator of X,Y
for T1 being Function of , st T1 = T & T1 is onto holds
T1 is open

let T be Lipschitzian LinearOperator of X,Y; :: thesis: for T1 being Function of , st T1 = T & T1 is onto holds
T1 is open

let T1 be Function of ,; :: thesis: ( T1 = T & T1 is onto implies T1 is open )
assume that
A1: T1 = T and
A2: T1 is onto ; :: thesis: T1 is open
thus for G being Subset of st G is open holds
T1 .: G is open :: according to T_0TOPSP:def 2 :: thesis: verum
proof
reconsider TB1 = T .: (Ball ((0. X),1)) as Subset of by NORMSP_2:def 4;
defpred S1[ Nat, set ] means ex TBn being Subset of () st
( TBn = T .: (Ball ((0. X),\$1)) & \$2 = Cl TBn );
let G be Subset of ; :: thesis: ( G is open implies T1 .: G is open )
A3: for n being Element of NAT ex y being Element of bool the carrier of Y st S1[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of bool the carrier of Y st S1[n,y]
reconsider TBn = T .: (Ball ((0. X),n)) as Subset of () ;
Cl TBn c= the carrier of Y ;
hence ex y being Element of bool the carrier of Y st S1[n,y] ; :: thesis: verum
end;
consider f being sequence of (bool the carrier of Y) such that
A4: for x being Element of NAT holds S1[x,f . x] from reconsider f = f as SetSequence of Y ;
A5: for n being Nat holds f . n is closed
proof
let n be Nat; :: thesis: f . n is closed
n in NAT by ORDINAL1:def 12;
then ex TBn being Subset of () st
( TBn = T .: (Ball ((0. X),n)) & f . n = Cl TBn ) by A4;
hence f . n is closed by NORMSP_2:15; :: thesis: verum
end;
A6: the carrier of Y c= union (rng f)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of Y or z in union (rng f) )
assume z in the carrier of Y ; :: thesis: z in union (rng f)
then reconsider z1 = z as Point of Y ;
rng T = the carrier of by ;
then rng T = the carrier of Y by NORMSP_2:def 4;
then consider x1 being object such that
A7: x1 in the carrier of X and
A8: z1 = T . x1 by FUNCT_2:11;
reconsider x1 = x1 as Point of X by A7;
consider m being Element of NAT such that
A9: ||.x1.|| <= m by MESFUNC1:8;
set n = m + 1;
||.x1.|| + 0 < m + 1 by ;
then ||.(- x1).|| < m + 1 by NORMSP_1:2;
then ||.((0. X) - x1).|| < m + 1 by RLVECT_1:14;
then x1 in Ball ((0. X),(m + 1)) ;
then A10: T . x1 in T .: (Ball ((0. X),(m + 1))) by FUNCT_2:35;
NAT = dom f by FUNCT_2:def 1;
then A11: f . (m + 1) in rng f by FUNCT_1:3;
consider TBn being Subset of () such that
A12: TBn = T .: (Ball ((0. X),(m + 1))) and
A13: f . (m + 1) = Cl TBn by A4;
TBn c= f . (m + 1) by ;
hence z in union (rng f) by ; :: thesis: verum
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 being Nat, r being Real, y0 being Point of Y such that
A14: 0 < r and
A15: Ball (y0,r) c= f . n0 by ;
n0 in NAT by ORDINAL1:def 12;
then consider TBn0 being Subset of () such that
A16: TBn0 = T .: (Ball ((0. X),n0)) and
A17: f . n0 = Cl TBn0 by A4;
consider TBn01 being Subset of () 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 ;
then TBn0 c= TBn01 by ;
then f . n0 c= f . (n0 + 1) by ;
then A20: Ball (y0,r) c= Cl TBn01 by ;
reconsider LTBn01 = TBn01 as Subset of 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 by NORMSP_2:def 4;
A22: Ball ((0. Y),(r / ((2 * n0) + 2))) is Subset of by NORMSP_2:def 4;
||.(y0 - y0).|| < r by ;
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 ;
reconsider TBnx01 = T .: (Ball ((0. X),(n0 + 1))) as Subset of by NORMSP_2:def 4;
reconsider BYyr = Ball (y0,r) as Subset of by NORMSP_2:def 4;
reconsider BYr = Ball ((0. Y),r) as Subset of 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
.= T .: ((- 1) * (Ball ((0. X),(n0 + 1)))) by Th5
.= LTBn01 by ;
then - yy0 in Cl LTBn01 by ;
then - yy0 in Cl TBn01 by Th10;
then {(- yy0)} c= Cl TBn01 by ZFMISC_1:31;
then A25: my0 c= Cl TBnx01 by ;
BYyr c= Cl TBnx01 by ;
then my0 + BYyr c= (Cl TBnx01) + (Cl TBnx01) by ;
then (- yy0) + BYyr c= (Cl TBnx01) + (Cl TBnx01) by RUSUB_4:33;
then A26: (- y0) + (Ball (y0,r)) c= (Cl TBnx01) + (Cl TBnx01) by ;
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 = () + BYr by RLVECT_1:5;
then (- yy0) + BYyr = {()} + BYr by RUSUB_4:33;
then (- yy0) + BYyr = BYr by CONVEX1:35;
then Ball ((0. Y),r) = (- y0) + (Ball (y0,r)) by ;
then A28: Ball ((0. Y),r) c= Cl (TBnx01 + TBnx01) by ;
TBnx01 = 1 * TBnx01 by CONVEX1:32;
then A29: TBnx01 + TBnx01 = (1 + 1) * TBnx01 by
.= 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
.= (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 ;
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 ;
(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 ;
A34: for p being Real st p > 0 holds
ex q being 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; :: thesis: ( p > 0 implies ex q being Real st
( 0 < q & Ball ((0. Y),q) c= T .: (Ball ((0. X),p)) ) )

assume A35: p > 0 ; :: thesis: ex q being Real st
( 0 < q & Ball ((0. Y),q) c= T .: (Ball ((0. X),p)) )

then A36: p * (Ball ((0. X),1)) = Ball ((0. X),(p * 1)) by Th3;
take (r / ((2 * n0) + 2)) * p ; :: thesis: ( 0 < (r / ((2 * n0) + 2)) * p & Ball ((0. Y),((r / ((2 * n0) + 2)) * p)) c= T .: (Ball ((0. X),p)) )
p * (Ball ((0. Y),(r / ((2 * n0) + 2)))) c= p * TB1 by ;
then Ball ((0. Y),((r / ((2 * n0) + 2)) * p)) c= p * TB1 by ;
hence ( 0 < (r / ((2 * n0) + 2)) * p & Ball ((0. Y),((r / ((2 * n0) + 2)) * p)) c= T .: (Ball ((0. X),p)) ) by ; :: thesis: verum
end;
assume A37: G is open ; :: thesis: T1 .: G is open
now :: thesis: for y being Point of Y st y in T1 .: G holds
ex q being Real st
( 0 < q & { w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G )
let y be Point of Y; :: thesis: ( y in T1 .: G implies ex q being Real st
( 0 < q & { w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G ) )

assume y in T1 .: G ; :: thesis: ex q being Real st
( 0 < q & { w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G )

then consider x being Point of X such that
A38: x in G and
A39: y = T . x by ;
consider p being Real such that
A40: p > 0 and
A41: { z where z is Point of X : ||.(x - z).|| < p } c= G by ;
reconsider TBp = T .: (Ball ((0. X),p)) as Subset of Y ;
consider q being Real such that
A42: 0 < q and
A43: Ball ((0. Y),q) c= TBp by ;
Ball (x,p) c= G by A41;
then A44: x + (Ball ((0. X),p)) c= G by Th2;
now :: thesis: for t being object st t in y + TBp holds
t in T1 .: G
let t be object ; :: thesis: ( t in y + TBp implies t in T1 .: G )
assume t in y + TBp ; :: thesis: t in T1 .: G
then consider tz0 being Point of Y such that
A45: t = y + tz0 and
A46: tz0 in TBp ;
consider z0 being Element of X such that
A47: z0 in Ball ((0. X),p) and
A48: tz0 = T . z0 by ;
reconsider z0 = z0 as Point of X ;
A49: x + z0 in x + (Ball ((0. X),p)) by A47;
t = T . (x + z0) by ;
hence t in T1 .: G by ; :: thesis: verum
end;
then A50: y + TBp c= T .: G by A1;
take q = q; :: thesis: ( 0 < q & { w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G )
now :: thesis: for t being object st t in y + (Ball ((0. Y),q)) holds
t in y + TBp
let t be object ; :: thesis: ( t in y + (Ball ((0. Y),q)) implies t in y + TBp )
assume t in y + (Ball ((0. Y),q)) ; :: thesis: t in y + TBp
then ex z0 being Point of Y st
( t = y + z0 & z0 in Ball ((0. Y),q) ) ;
hence t in y + TBp by A43; :: thesis: verum
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 is Point of Y : ||.(y - w).|| < q } c= T1 .: G ) by A1, A50, A42; :: thesis: verum
end;
hence T1 .: G is open by NORMSP_2:22; :: thesis: verum
end;