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;
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