let X, Y be RealBanachSpace; :: thesis:
let T be Lipschitzian LinearOperator of X,Y; :: thesis:
let T1 be Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y); :: thesis:
assume that
A1: T1 = T and
A2: T1 is onto ; :: thesis:
thus for G being Subset of (LinearTopSpaceNorm X) st G is open holds
T1 .: G is open :: according to T_0TOPSP:def 2 :: thesis:

proof

reconsider TB1 = T .: (Ball ((0. X),1)) as Subset of (LinearTopSpaceNorm Y) by NORMSP_2:def 4;
defpred S₁[ Nat, set ] means ex TBn being Subset of (TopSpaceNorm Y) st
( TBn = T .: (Ball ((0. X),$1)) & $2 = Cl TBn );
let G be Subset of (LinearTopSpaceNorm X); :: thesis:
A3: for n being Element of NAT ex y being Element of bool the carrier of Y st S₁[n,y]

proof

let n be Element of NAT ; :: thesis:
reconsider TBn = T .: (Ball ((0. X),n)) as Subset of (TopSpaceNorm Y) ;
Cl TBn c= the carrier of Y ;
hence ex y being Element of bool the carrier of Y st S₁[n,y] ; :: thesis:

end;

consider f being sequence of (bool the carrier of Y) such that
A4: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
reconsider f = f as SetSequence of Y ;
A5: for n being Nat holds f . n is closed

proof

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
then ex TBn being Subset of (TopSpaceNorm Y) st
( TBn = T .: (Ball ((0. X),n)) & f . n = Cl TBn ) by A4;
hence f . n is closed by NORMSP_2:15; :: thesis:

end;

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in the carrier of Y ; :: thesis:
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 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 A9, XREAL_1:8;
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 (TopSpaceNorm Y) 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 A13, PRE_TOPC:18;
hence z in union (rng f) by A8, A10, A12, A11, TARSKI:def 4; :: thesis:

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 A5, LOPBAN_5:3;
n0 in NAT by ORDINAL1:def 12;
then consider TBn0 being Subset of (TopSpaceNorm Y) such that
A16: TBn0 = T .: (Ball ((0. X),n0)) and
A17: f . n0 = Cl TBn0 by A4;
consider TBn01 being 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 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:
assume A35: p > 0 ; :: thesis:
then A36: p * (Ball ((0. X),1)) = Ball ((0. X),(p * 1)) by Th3;
take (r / ((2 * n0) + 2)) * p ; :: thesis:
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 ( 0 < (r / ((2 * n0) + 2)) * p & Ball ((0. Y),((r / ((2 * n0) + 2)) * p)) c= T .: (Ball ((0. X),p)) ) by A31, A35, A36, Th5, XREAL_1:129; :: thesis:

end;

assume A37: G is open ; :: thesis:

now :: thesis:

let y be Point of Y; :: thesis:
assume y in T1 .: G ; :: thesis:
then consider x being Point of X such that
A38: x in G and
A39: y = T . x by A1, FUNCT_2:65;
consider p being Real such that
A40: p > 0 and
A41: { z where z is 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 being 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 :: thesis:

let t be object ; :: thesis:
assume t in y + TBp ; :: thesis:
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 A46, FUNCT_2:65;
reconsider z0 = 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; :: thesis:

end;

then A50: y + TBp c= T .: G by A1;
take q = q; :: thesis:

now :: thesis:

let t be object ; :: thesis:
assume t in y + (Ball ((0. Y),q)) ; :: thesis:
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:

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:

end;

hence T1 .: G is open by NORMSP_2:22; :: thesis:

end;