let X, Y be RealBanachSpace; :: thesis: for T being Lipschitzian LinearOperator of X,Y

for T1 being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st T1 = T & T1 is onto holds

T1 is open

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

T1 is open

let T1 be Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y); :: 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 (LinearTopSpaceNorm X) st G is open holds

T1 .: G is open :: according to T_0TOPSP:def 2 :: thesis: verum

for T1 being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st T1 = T & T1 is onto holds

T1 is open

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

T1 is open

let T1 be Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y); :: 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 (LinearTopSpaceNorm X) 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 (LinearTopSpaceNorm Y) by NORMSP_2:def 4;

defpred S_{1}[ 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: ( 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 S_{1}[n,y]

A4: for x being Element of NAT holds S_{1}[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

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)) )

end;defpred S

( TBn = T .: (Ball ((0. X),$1)) & $2 = Cl TBn );

let G be Subset of (LinearTopSpaceNorm X); :: 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 S

proof

consider f being sequence of (bool the carrier of Y) such that
let n be Element of NAT ; :: thesis: ex y being Element of bool the carrier of Y st S_{1}[n,y]

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_{1}[n,y]
; :: thesis: verum

end;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

A4: for x being Element of NAT holds S

reconsider f = f as SetSequence of Y ;

A5: for n being Nat holds f . n is closed

proof

A6:
the carrier of Y c= union (rng f)
let n be Nat; :: thesis: f . n is closed

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: verum

end;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: verum

proof

union (rng f) is Subset of Y
by PROB_1:11;
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 (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: verum

end;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 (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: verum

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

assume A37:
G is open
; :: thesis: T1 .: G is open
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 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: verum

end;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 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: verum

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 )

hence
T1 .: G is open
by NORMSP_2:22; :: thesis: verumex 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 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;

take q = q; :: thesis: ( 0 < q & { w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G )

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;( 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 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: for t being object st t in y + TBp holds

t in T1 .: G

then A50:
y + TBp c= T .: G
by A1;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 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: verum

end;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 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: verum

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

then
y + (Ball ((0. Y),q)) c= y + TBp
;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;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

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