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