let n, m be Nat; :: thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for B being OrdBasis of Lin (lines M) st B = M holds
for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
let f be n -element real-valued FinSequence; :: thesis: for M being Matrix of n,m,F_Real
for B being OrdBasis of Lin (lines M) st B = M holds
for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
let M be Matrix of n,m,F_Real; :: thesis: for B being OrdBasis of Lin (lines M) st B = M holds
for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
set LM = lines M;
let B be OrdBasis of Lin (lines M); :: thesis: ( B = M implies for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f )
assume A1: B = M ; :: thesis: for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
A2: B is one-to-one by MATRLIN:def 2;
let Mf be Element of (Lin (lines M)); :: thesis: ( Mf = (Mx2Tran M) . f implies Mf |-- B = f )
assume A3: Mf = (Mx2Tran M) . f ; :: thesis: Mf |-- B = f
consider L being Linear_Combination of lines M such that
A4: Sum L = Mf and
A5: for i being Nat st i in dom f holds
L . (Line (M,i)) = f . i by A1, A3, A2, Th16;
reconsider L1 = L | the carrier of (Lin (lines M)) as Linear_Combination of Lin (lines M) by Th8;
A6: len M = n by MATRIX_0:def 2;
A7: len f = n by CARD_1:def 7;
A8: lines M c= [#] (Lin (lines M)) by Lm4;

A9: now :: thesis: for k being Nat st 1 <= k & k <= n holds
(@ f) /. k = L1 . (B /. k)

let k be Nat; :: thesis: ( 1 <= k & k <= n implies (@ f) /. k = L1 . (B /. k) )
assume A10: ( 1 <= k & k <= n ) ; :: thesis: (@ f) /. k = L1 . (B /. k)
then k in Seg n ;
then A11: M . k = Line (M,k) by MATRIX_0:52;
A12: k in dom M by A6, A10, FINSEQ_3:25;
then A13: B /. k = M . k by A1, PARTFUN1:def 6;
M . k in lines M by A12, FUNCT_1:def 3;
then A14: L . (M . k) = L1 . (M . k) by A8, FUNCT_1:49;
A15: k in dom f by A7, A10, FINSEQ_3:25;
then f . k = (@ f) /. k by PARTFUN1:def 6;
hence (@ f) /. k = L1 . (B /. k) by A5, A15, A13, A11, A14; :: thesis: verum

end;

A16: Carrier L c= lines M by VECTSP_6:def 4;
then Carrier L c= [#] (Lin (lines M)) by A8;
then ( Carrier L = Carrier L1 & Sum L1 = Sum L ) by VECTSP_9:7;
hence Mf |-- B = f by A1, A4, A6, A7, A16, A9, MATRLIN:def 7; :: thesis: verum