let n, m be Nat; 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; 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; ( 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
; ((Mx2Tran M) . f) | n = f
per cases
( n = 0 or n > 0 )
;
suppose A3:
n > 0
;
((Mx2Tran M) . f) | n = fset 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;
verum end;