let n, m be Nat; :: thesis: for f being n -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
let f be n -element real-valued FinSequence; :: thesis: for M being Matrix of n,m,F_Real st M = (1. (F_Real,m)) | n holds
((Mx2Tran M) . f) | n = f
let M be Matrix of n,m,F_Real; :: thesis: ( M = (1. (F_Real,m)) | n implies ((Mx2Tran M) . f) | n = f )
set ONE = 1. (F_Real,m);
assume A1: M = (1. (F_Real,m)) | n ; :: thesis: ((Mx2Tran M) . f) | n = f

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

suppose A2: n = 0 ; :: thesis: ((Mx2Tran M) . f) | n = f

then ((Mx2Tran M) . f) | n is empty ;
hence ((Mx2Tran M) . f) | n = f by A2; :: thesis: verum

end;

suppose A3: n > 0 ; :: thesis: ((Mx2Tran M) . f) | n = f

set TRm = TOP-REAL m;
set V = m -VectSp_over F_Real;
A4: len (1. (F_Real,m)) = m by MATRIX_0:24;
A5: len f = n by CARD_1:def 7;
consider A being FinSequence such that
A6: 1. (F_Real,m) = M ^ A by A1, FINSEQ_1:80;
1. (F_Real,m) = MX2FinS (1. (F_Real,m)) ;
then reconsider A = A as FinSequence of (m -VectSp_over F_Real) by A6, FINSEQ_1:36;
set L = len A;
len M = n by A3, MATRIX13:1;
then n + (len A) = m by A4, A6, FINSEQ_1:22;
then A7: f ^ ((len A) |-> 0) is Element of (TOP-REAL m) by Lm2;
set A1 = FinS2MX A;
A8: (f ^ ((len A) |-> 0)) | n = (f ^ ((len A) |-> 0)) | (dom f) by A5, FINSEQ_1:def 3
.= f by FINSEQ_1:21 ;
(Mx2Tran (M ^ (FinS2MX A))) . (f ^ ((len A) |-> 0)) = (Mx2Tran (1. (F_Real,m))) . (f ^ ((len A) |-> 0)) by A3, A4, A6, MATRIX13:1
.= (id (TOP-REAL m)) . (f ^ ((len A) |-> 0)) by Th33
.= f ^ ((len A) |-> 0) by A7 ;
hence ((Mx2Tran M) . f) | n = f by A8, Th35; :: thesis: verum

end;

end;