let n, m be Nat; for M being Matrix of n,m,F_Real holds Mx2Tran M is continuous
let M be Matrix of n,m,F_Real; Mx2Tran M is continuous
set Tn = TOP-REAL n;
set Tm = TOP-REAL m;
set TM = Mx2Tran M;
consider L being Real such that
A1:
L > 0
and
A2:
for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.|
by Th45;
let x be Point of (TOP-REAL n); BORSUK_1:def 1 for b1 being a_neighborhood of (Mx2Tran M) . x ex b2 being a_neighborhood of x st K784( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m),(Mx2Tran M),b2) c= b1
let U be a_neighborhood of (Mx2Tran M) . x; ex b1 being a_neighborhood of x st K784( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m),(Mx2Tran M),b1) c= U
reconsider TMx = (Mx2Tran M) . x as Point of (TOP-REAL m) ;
reconsider tmx = TMx as Point of (Euclid m) by EUCLID:67;
reconsider X = x as Point of (Euclid n) by EUCLID:67;
tmx in Int U
by CONNSP_2:def 1;
then consider r being Real such that
A3:
r > 0
and
A4:
Ball (tmx,r) c= U
by GOBOARD6:5;
reconsider B = Ball (X,(r / L)) as Subset of (TOP-REAL n) by EUCLID:67;
r / L > 0
by A3, A1, XREAL_1:139;
then
x in Int B
by GOBOARD6:5;
then reconsider Bx = B as a_neighborhood of x by CONNSP_2:def 1;
take
Bx
; K784( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m),(Mx2Tran M),Bx) c= U
let y be object ; TARSKI:def 3 ( not y in K784( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m),(Mx2Tran M),Bx) or y in U )
assume
y in (Mx2Tran M) .: Bx
; y in U
then consider p being object such that
p in dom (Mx2Tran M)
and
A5:
p in Bx
and
A6:
(Mx2Tran M) . p = y
by FUNCT_1:def 6;
reconsider p = p as Point of (TOP-REAL n) by A5;
A7:
(r / L) * L = r
by A1, XCMPLX_1:87;
reconsider TMp = (Mx2Tran M) . p as Point of (TOP-REAL m) ;
reconsider tmp = TMp as Point of (Euclid m) by EUCLID:67;
dist (tmx,tmp) =
|.(((Mx2Tran M) . x) - ((Mx2Tran M) . p)).|
by SPPOL_1:39
.=
|.((Mx2Tran M) . (x - p)).|
by Th28
;
then A8:
dist (tmx,tmp) <= L * |.(x - p).|
by A2;
reconsider P = p as Point of (Euclid n) by EUCLID:67;
dist (X,P) < r / L
by A5, METRIC_1:11;
then A9:
(dist (X,P)) * L < (r / L) * L
by A1, XREAL_1:68;
dist (X,P) = |.(x - p).|
by SPPOL_1:39;
then
dist (tmx,tmp) < r
by A9, A7, A8, XXREAL_0:2;
then
tmp in Ball (tmx,r)
by METRIC_1:11;
hence
y in U
by A4, A6; verum