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;
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); :: according to BORSUK_1:def 1 :: thesis: for b₁ being a_neighborhood of (Mx2Tran M) . x ex b₂ being a_neighborhood of x st K787( 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 K787( 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;
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 ; :: thesis: K787( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m),(Mx2Tran M),Bx) c= U
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in K787( 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 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; :: thesis: verum