let n, m be Nat; :: thesis: 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)
let M be Matrix of n,m,F_Real; :: thesis: 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)
let Bn be OrdBasis of n -VectSp_over F_Real; :: thesis: 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)
let Bm be OrdBasis of m -VectSp_over F_Real; :: thesis: ( Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) implies for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm) )
assume that
A1: Bn = MX2FinS (1. (F_Real,n)) and
A2: Bm = MX2FinS (1. (F_Real,m)) ; :: thesis: for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
set T = Mx2Tran M;
let M1 be Matrix of len Bn, len Bm,F_Real; :: thesis: ( M1 = M implies Mx2Tran M = Mx2Tran (M1,Bn,Bm) )
assume A3: M1 = M ; :: thesis: Mx2Tran M = Mx2Tran (M1,Bn,Bm)
set Tb = Mx2Tran (M1,Bn,Bm);
dom (Mx2Tran (M1,Bn,Bm)) = the carrier of (n -VectSp_over F_Real) by FUNCT_2:def 1;
then A4: dom (Mx2Tran (M1,Bn,Bm)) = REAL n by MATRIX13:102
.= the carrier of (TOP-REAL n) by EUCLID:22 ;
A5: for x being object st x in dom (Mx2Tran M) holds
(Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x

proof

let x be object ; :: thesis: ( x in dom (Mx2Tran M) implies (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x )
assume x in dom (Mx2Tran M) ; :: thesis: (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x
then reconsider v = x as Element of (TOP-REAL n) by FUNCT_2:def 1;
reconsider g = v as Vector of (n -VectSp_over F_Real) by A4, FUNCT_2:def 1;
set L = LineVec2Mx (@ v);
len v = n by CARD_1:def 7;
then A6: ( len (LineVec2Mx (@ v)) = 1 & width (LineVec2Mx (@ v)) = n ) by MATRIX13:1;
A7: len Bn = n by A1, Th19;
A8: len Bm = m by A2, Th19;

per cases ( n = 0 or n > 0 ) ;

suppose A9: n = 0 ; :: thesis: (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x

then (Mx2Tran (M1,Bn,Bm)) . g = 0. (m -VectSp_over F_Real) by A1, Th19, MATRLIN2:33
.= m |-> (0. F_Real) by MATRIX13:102
.= 0* m
.= 0. (TOP-REAL m) by EUCLID:70
.= (Mx2Tran M) . v by A9, Def3 ;
hence (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x ; :: thesis: verum

end;

suppose A10: n > 0 ; :: thesis: (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x

A11: ((Mx2Tran (M1,Bn,Bm)) . g) |-- Bm = (Mx2Tran (M1,Bn,Bm)) . g by A2, A8, MATRLIN2:46;
A12: ( g |-- Bn = g & AutMt ((Mx2Tran (M1,Bn,Bm)),Bn,Bm) = M ) by A1, A3, A7, MATRLIN2:36, MATRLIN2:46;
( 1 in dom (LineVec2Mx (@ v)) & len M = width (LineVec2Mx (@ v)) ) by A10, A6, FINSEQ_3:25, MATRIX13:1;
then LineVec2Mx (Line (((LineVec2Mx (@ v)) * M),1)) = (LineVec2Mx (Line ((LineVec2Mx (@ v)),1))) * M by MATRLIN2:35
.= (LineVec2Mx (@ v)) * M by MATRIX15:25
.= LineVec2Mx (((Mx2Tran (M1,Bn,Bm)) . g) |-- Bm) by A7, A10, A12, MATRLIN2:31 ;
hence (Mx2Tran (M1,Bn,Bm)) . x = Line ((LineVec2Mx (Line (((LineVec2Mx (@ v)) * M),1))),1) by A11, MATRIX15:25
.= Line (((LineVec2Mx (@ v)) * M),1) by MATRIX15:25
.= (Mx2Tran M) . x by A10, Def3 ;
:: thesis: verum

end;

end;

end;

dom (Mx2Tran M) = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
hence Mx2Tran M = Mx2Tran (M1,Bn,Bm) by A4, A5, FUNCT_1:2; :: thesis: verum