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
A3: 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 A4: Mf = (Mx2Tran M) . f ; :: thesis: Mf |-- B = f
consider L being Linear_Combination of lines M such that
A5: Sum L = Mf and
A6: for i being Nat st i in dom f holds
L . (Line (M,i)) = f . i by A1, A4, A3, Th16;
reconsider L1 = L | the carrier of (Lin (lines M)) as Linear_Combination of Lin (lines M) by Th8;
A7: len M = n by MATRIX_1:def 2;
A8: len f = n by CARD_1:def 7;
A9: lines M c= [#] (Lin (lines M)) by Lm4;

A10: now

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

end;

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