:: by Karol P\kak

::

:: Received October 26, 2010

:: Copyright (c) 2010-2012 Association of Mizar Users

begin

registration

let X, Y be set ;

let F be positive-yielding PartFunc of X,REAL;

coherence

F | Y is positive-yielding

end;
let F be positive-yielding PartFunc of X,REAL;

coherence

F | Y is positive-yielding

proof end;

registration

let X, Y be set ;

let F be negative-yielding PartFunc of X,REAL;

coherence

F | Y is negative-yielding

end;
let F be negative-yielding PartFunc of X,REAL;

coherence

F | Y is negative-yielding

proof end;

registration

let X, Y be set ;

let F be nonpositive-yielding PartFunc of X,REAL;

coherence

F | Y is nonpositive-yielding

end;
let F be nonpositive-yielding PartFunc of X,REAL;

coherence

F | Y is nonpositive-yielding

proof end;

registration

let X, Y be set ;

let F be nonnegative-yielding PartFunc of X,REAL;

coherence

F | Y is nonnegative-yielding

end;
let F be nonnegative-yielding PartFunc of X,REAL;

coherence

F | Y is nonnegative-yielding

proof end;

registration
end;

theorem :: MATRTOP1:1

theorem Th5: :: MATRTOP1:5

for rf being real-valued FinSequence st rf is nonnegative-yielding holds

sqrt (Sum rf) <= Sum (sqrt rf)

sqrt (Sum rf) <= Sum (sqrt rf)

proof end;

registration
end;

registration
end;

theorem Th7: :: MATRTOP1:7

for X being set

for f, f1 being FinSequence

for P being Permutation of (dom f) st f1 = f * P holds

ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q

for f, f1 being FinSequence

for P being Permutation of (dom f) st f1 = f * P holds

ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q

proof end;

theorem :: MATRTOP1:8

for X being set

for cf, cf1 being complex-valued FinSequence

for P being Permutation of (dom cf) st cf1 = cf * P holds

Sum (cf1 - X) = Sum (cf - X)

for cf, cf1 being complex-valued FinSequence

for P being Permutation of (dom cf) st cf1 = cf * P holds

Sum (cf1 - X) = Sum (cf - X)

proof end;

theorem Th9: :: MATRTOP1:9

for X being set

for f, f1 being FinSubsequence

for P being Permutation of (dom f) st f1 = f * P holds

ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q

for f, f1 being FinSubsequence

for P being Permutation of (dom f) st f1 = f * P holds

ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q

proof end;

theorem :: MATRTOP1:10

for X being set

for cf, cf1 being complex-valued FinSubsequence

for P being Permutation of (dom cf) st cf1 = cf * P holds

Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))

for cf, cf1 being complex-valued FinSubsequence

for P being Permutation of (dom cf) st cf1 = cf * P holds

Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))

proof end;

theorem Th11: :: MATRTOP1:11

for X, Y being set

for f being FinSubsequence

for n being Element of NAT st ( for i being Nat holds

( i + n in X iff i in Y ) ) holds

(n Shift f) | X = n Shift (f | Y)

for f being FinSubsequence

for n being Element of NAT st ( for i being Nat holds

( i + n in X iff i in Y ) ) holds

(n Shift f) | X = n Shift (f | Y)

proof end;

theorem Th12: :: MATRTOP1:12

for X being set

for f1, f2 being FinSequence ex Y being Subset of NAT st

( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y)) & ( for n being Nat st n > 0 holds

( n in Y iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )

for f1, f2 being FinSequence ex Y being Subset of NAT st

( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y)) & ( for n being Nat st n > 0 holds

( n in Y iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )

proof end;

theorem :: MATRTOP1:13

for X being set

for g1, f1, g2, f2 being FinSequence st len g1 = len f1 & len g2 <= len f2 holds

Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X)))

for g1, f1, g2, f2 being FinSequence st len g1 = len f1 & len g2 <= len f2 holds

Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X)))

proof end;

theorem :: MATRTOP1:14

for X being set

for n, m being Nat

for D being non empty set

for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D

for n, m being Nat

for D being non empty set

for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D

proof end;

theorem Th15: :: MATRTOP1:15

for n, m being Nat

for F being Function of (Seg n),(Seg n)

for D being non empty set

for M being Matrix of n,m,D

for i being Nat st i in Seg (width M) holds

Col ((M * F),i) = (Col (M,i)) * F

for F being Function of (Seg n),(Seg n)

for D being non empty set

for M being Matrix of n,m,D

for i being Nat st i in Seg (width M) holds

Col ((M * F),i) = (Col (M,i)) * F

proof end;

Lm1: for n, m being Nat

for K being Field

for A being Matrix of n,m,K st ( n = 0 implies m = 0 ) & the_rank_of A = n holds

ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m

proof end;

theorem Th16: :: MATRTOP1:16

for n, m being Nat

for K being Field

for A being Matrix of n,m,K st the_rank_of A = n holds

ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m

for K being Field

for A being Matrix of n,m,K st the_rank_of A = n holds

ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m

proof end;

theorem :: MATRTOP1:17

for n, m being Nat

for K being Field

for A being Matrix of n,m,K st the_rank_of A = m holds

ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n

for K being Field

for A being Matrix of n,m,K st the_rank_of A = m holds

ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n

proof end;

Lm2: for n being Nat

for f being b

proof end;

begin

:: given by a Transformation Matrix

definition

let n, m be Nat;

let M be Matrix of n,m,F_Real;

( ( n <> 0 implies ex b_{1} being Function of (TOP-REAL n),(TOP-REAL m) st

for f being n -element real-valued FinSequence holds b_{1} . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( not n <> 0 implies ex b_{1} being Function of (TOP-REAL n),(TOP-REAL m) st

for f being n -element real-valued FinSequence holds b_{1} . f = 0. (TOP-REAL m) ) )

for b_{1}, b_{2} being Function of (TOP-REAL n),(TOP-REAL m) holds

( ( n <> 0 & ( for f being n -element real-valued FinSequence holds b_{1} . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds b_{2} . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies b_{1} = b_{2} ) & ( not n <> 0 & ( for f being n -element real-valued FinSequence holds b_{1} . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds b_{2} . f = 0. (TOP-REAL m) ) implies b_{1} = b_{2} ) )

consistency

for b_{1} being Function of (TOP-REAL n),(TOP-REAL m) holds verum;

;

end;
let M be Matrix of n,m,F_Real;

func Mx2Tran M -> Function of (TOP-REAL n),(TOP-REAL m) means :Def3: :: MATRTOP1:def 3

for f being n -element real-valued FinSequence holds it . f = Line (((LineVec2Mx (@ f)) * M),1) if n <> 0

otherwise for f being n -element real-valued FinSequence holds it . f = 0. (TOP-REAL m);

existence for f being n -element real-valued FinSequence holds it . f = Line (((LineVec2Mx (@ f)) * M),1) if n <> 0

otherwise for f being n -element real-valued FinSequence holds it . f = 0. (TOP-REAL m);

( ( n <> 0 implies ex b

for f being n -element real-valued FinSequence holds b

for f being n -element real-valued FinSequence holds b

proof end;

uniqueness for b

( ( n <> 0 & ( for f being n -element real-valued FinSequence holds b

proof end;

correctness consistency

for b

;

:: deftheorem Def3 defines Mx2Tran MATRTOP1:def 3 :

for n, m being Nat

for M being Matrix of n,m,F_Real

for b_{4} being Function of (TOP-REAL n),(TOP-REAL m) holds

( ( n <> 0 implies ( b_{4} = Mx2Tran M iff for f being b_{1} -element real-valued FinSequence holds b_{4} . f = Line (((LineVec2Mx (@ f)) * M),1) ) ) & ( not n <> 0 implies ( b_{4} = Mx2Tran M iff for f being b_{1} -element real-valued FinSequence holds b_{4} . f = 0. (TOP-REAL m) ) ) );

for n, m being Nat

for M being Matrix of n,m,F_Real

for b

( ( n <> 0 implies ( b

Lm3: now :: thesis: for n, m being Nat

for M being Matrix of n,m,F_Real

for x being set holds (Mx2Tran M) . x is real-valued FinSequence

for M being Matrix of n,m,F_Real

for x being set holds (Mx2Tran M) . x is real-valued FinSequence

let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real

for x being set holds (Mx2Tran b_{5}) . b_{6} is real-valued FinSequence

let M be Matrix of n,m,F_Real; :: thesis: for x being set holds (Mx2Tran b_{4}) . b_{5} is real-valued FinSequence

let x be set ; :: thesis: (Mx2Tran b_{3}) . b_{4} is real-valued FinSequence

set T = Mx2Tran M;

end;
for x being set holds (Mx2Tran b

let M be Matrix of n,m,F_Real; :: thesis: for x being set holds (Mx2Tran b

let x be set ; :: thesis: (Mx2Tran b

set T = Mx2Tran M;

per cases
( x in dom (Mx2Tran M) or not x in dom (Mx2Tran M) )
;

end;

suppose A1:
x in dom (Mx2Tran M)
; :: thesis: (Mx2Tran b_{3}) . b_{4} is real-valued FinSequence

A2:
rng (Mx2Tran M) c= the carrier of (TOP-REAL m)
by RELAT_1:def 19;

(Mx2Tran M) . x in rng (Mx2Tran M) by A1, FUNCT_1:def 3;

hence (Mx2Tran M) . x is real-valued FinSequence by A2; :: thesis: verum

end;
(Mx2Tran M) . x in rng (Mx2Tran M) by A1, FUNCT_1:def 3;

hence (Mx2Tran M) . x is real-valued FinSequence by A2; :: thesis: verum

suppose
not x in dom (Mx2Tran M)
; :: thesis: (Mx2Tran b_{3}) . b_{4} is real-valued FinSequence

end;

end;

registration

let n, m be Nat;

let M be Matrix of n,m,F_Real;

let x be set ;

coherence

( (Mx2Tran M) . x is Function-like & (Mx2Tran M) . x is Relation-like ) by Lm3;

coherence

( (Mx2Tran M) . x is real-valued & (Mx2Tran M) . x is FinSequence-like ) by Lm3;

end;
let M be Matrix of n,m,F_Real;

let x be set ;

coherence

( (Mx2Tran M) . x is Function-like & (Mx2Tran M) . x is Relation-like ) by Lm3;

coherence

( (Mx2Tran M) . x is real-valued & (Mx2Tran M) . x is FinSequence-like ) by Lm3;

registration

let n, m be Nat;

let M be Matrix of n,m,F_Real;

let f be n -element real-valued FinSequence;

coherence

(Mx2Tran M) . f is m -element

end;
let M be Matrix of n,m,F_Real;

let f be n -element real-valued FinSequence;

coherence

(Mx2Tran M) . f is m -element

proof end;

theorem Th18: :: MATRTOP1:18

for i, m, n being Nat

for f being b_{3} -element real-valued FinSequence

for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds

((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))

for f being b

for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds

((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))

proof end;

theorem Th20: :: MATRTOP1:20

for n, m being Nat

for M being Matrix of n,m,F_Real

for Bn being OrdBasis of n -VectSp_over F_Real

for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds

for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds

Mx2Tran M = Mx2Tran (M1,Bn,Bm)

for M being Matrix of n,m,F_Real

for Bn being OrdBasis of n -VectSp_over F_Real

for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds

for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds

Mx2Tran M = Mx2Tran (M1,Bn,Bm)

proof end;

theorem :: MATRTOP1:21

for m, n being Nat

for f being b_{2} -element real-valued FinSequence

for M being Matrix of n,m,F_Real

for P being Permutation of (Seg n) holds

( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is b_{2} -element FinSequence of REAL )

for f being b

for M being Matrix of n,m,F_Real

for P being Permutation of (Seg n) holds

( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is b

proof end;

theorem Th22: :: MATRTOP1:22

for n, m being Nat

for f1, f2 being b_{1} -element real-valued FinSequence

for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)

for f1, f2 being b

for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)

proof end;

theorem Th23: :: MATRTOP1:23

for n, m being Nat

for r being real number

for f being b_{1} -element real-valued FinSequence

for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)

for r being real number

for f being b

for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)

proof end;

theorem Th24: :: MATRTOP1:24

for n, m being Nat

for f1, f2 being b_{1} -element real-valued FinSequence

for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)

for f1, f2 being b

for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)

proof end;

theorem :: MATRTOP1:25

for n, m being Nat

for f being b_{1} -element real-valued FinSequence

for M1, M2 being Matrix of n,m,F_Real holds (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)

for f being b

for M1, M2 being Matrix of n,m,F_Real holds (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)

proof end;

theorem :: MATRTOP1:26

for n, m being Nat

for r being real number

for R being Element of F_Real

for f being b_{1} -element real-valued FinSequence

for M being Matrix of n,m,F_Real st r = R holds

r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f

for r being real number

for R being Element of F_Real

for f being b

for M being Matrix of n,m,F_Real st r = R holds

r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f

proof end;

theorem Th29: :: MATRTOP1:29

for n, m being Nat

for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)

for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)

proof end;

theorem :: MATRTOP1:30

for m, n being Nat

for p being Point of (TOP-REAL n)

for M being Matrix of n,m,F_Real

for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)

for p being Point of (TOP-REAL n)

for M being Matrix of n,m,F_Real

for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)

proof end;

theorem :: MATRTOP1:31

for n, m being Nat

for p being Point of (TOP-REAL n)

for M being Matrix of n,m,F_Real

for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)

for p being Point of (TOP-REAL n)

for M being Matrix of n,m,F_Real

for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)

proof end;

theorem Th32: :: MATRTOP1:32

for n, m, k being Nat

for A being Matrix of n,m,F_Real

for B being Matrix of width A,k,F_Real st ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) holds

(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)

for A being Matrix of n,m,F_Real

for B being Matrix of width A,k,F_Real st ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) holds

(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)

proof end;

theorem Th35: :: MATRTOP1:35

for n, m, k being Nat

for f being b_{1} -element real-valued FinSequence

for A being Matrix of n,m,F_Real

for B being Matrix of k,m,F_Real holds

( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )

for f being b

for A being Matrix of n,m,F_Real

for B being Matrix of k,m,F_Real holds

( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )

proof end;

theorem :: MATRTOP1:36

for n, m, k being Nat

for f being b_{1} -element real-valued FinSequence

for A being Matrix of n,m,F_Real

for B being Matrix of k,m,F_Real

for g being b_{3} -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)

for f being b

for A being Matrix of n,m,F_Real

for B being Matrix of k,m,F_Real

for g being b

proof end;

theorem :: MATRTOP1:37

for n, k, m being Nat

for f being b_{1} -element real-valued FinSequence

for A being Matrix of n,k,F_Real

for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds

(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)

for f being b

for A being Matrix of n,k,F_Real

for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds

(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)

proof end;

theorem :: MATRTOP1:38

for m, n being Nat

for f being b_{2} -element real-valued FinSequence

for M being Matrix of n,m,F_Real st M = (1. (F_Real,m)) | n holds

((Mx2Tran M) . f) | n = f

for f being b

for M being Matrix of n,m,F_Real st M = (1. (F_Real,m)) | n holds

((Mx2Tran M) . f) | n = f

proof end;

begin

theorem Th39: :: MATRTOP1:39

for m, n being Nat

for M being Matrix of n,m,F_Real holds

( Mx2Tran M is one-to-one iff the_rank_of M = n )

for M being Matrix of n,m,F_Real holds

( Mx2Tran M is one-to-one iff the_rank_of M = n )

proof end;

theorem Th40: :: MATRTOP1:40

for n being Nat

for A being Matrix of n,F_Real holds

( Mx2Tran A is one-to-one iff Det A <> 0. F_Real )

for A being Matrix of n,F_Real holds

( Mx2Tran A is one-to-one iff Det A <> 0. F_Real )

proof end;

theorem Th41: :: MATRTOP1:41

for n, m being Nat

for M being Matrix of n,m,F_Real holds

( Mx2Tran M is onto iff the_rank_of M = m )

for M being Matrix of n,m,F_Real holds

( Mx2Tran M is onto iff the_rank_of M = m )

proof end;

theorem Th43: :: MATRTOP1:43

for n being Nat

for A, B being Matrix of n,F_Real st Det A <> 0. F_Real holds

( (Mx2Tran A) " = Mx2Tran B iff A ~ = B )

for A, B being Matrix of n,F_Real st Det A <> 0. F_Real holds

( (Mx2Tran A) " = Mx2Tran B iff A ~ = B )

proof end;

Lm4: for n, m being Nat

for M being Matrix of n,m,F_Real

for f being b

( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds

L . i = |.(@ (Col (M,i))).| ) )

proof end;

theorem Th44: :: MATRTOP1:44

for m, n being Nat

for M being Matrix of n,m,F_Real ex L being b_{1} -element FinSequence of REAL st

( ( for i being Nat st i in dom L holds

L . i = |.(@ (Col (M,i))).| ) & ( for f being b_{2} -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )

for M being Matrix of n,m,F_Real ex L being b

( ( for i being Nat st i in dom L holds

L . i = |.(@ (Col (M,i))).| ) & ( for f being b

proof end;

theorem Th45: :: MATRTOP1:45

for m, n being Nat

for M being Matrix of n,m,F_Real ex L being Real st

( L > 0 & ( for f being b_{2} -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.| ) )

for M being Matrix of n,m,F_Real ex L being Real st

( L > 0 & ( for f being b

proof end;

theorem :: MATRTOP1:46

for m, n being Nat

for M being Matrix of n,m,F_Real st the_rank_of M = n holds

ex L being Real st

( L > 0 & ( for f being b_{2} -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )

for M being Matrix of n,m,F_Real st the_rank_of M = n holds

ex L being Real st

( L > 0 & ( for f being b

proof end;

registration

let n be Nat;

let K be Field;

ex b_{1} being Matrix of n,K st b_{1} is invertible

end;
let K be Field;

cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular invertible for Matrix of n,n, the carrier of K;

existence ex b

proof end;

registration

let n be Nat;

let A be invertible Matrix of n,F_Real;

coherence

Mx2Tran A is being_homeomorphism

end;
let A be invertible Matrix of n,F_Real;

coherence

Mx2Tran A is being_homeomorphism

proof end;