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 is one-to-one holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
let f be n -element real-valued FinSequence; :: thesis: for M being Matrix of n,m,F_Real st M is one-to-one holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
let M be Matrix of n,m,F_Real; :: thesis: ( M is one-to-one implies ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) ) )
assume A2: M is one-to-one ; :: thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
A3: len M = n by MATRIX_1:def 2;
then dom M c= Seg n by FINSEQ_1:def 3;
then reconsider D = dom M as Subset of (Seg n) ;
len f = n by CARD_1:def 7;
then A4: dom f = dom M by A3, FINSEQ_3:29;
M | (dom M) = M by RELAT_1:69;
then consider L being Linear_Combination of lines M such that
A5: Sum L = (Mx2Tran M) . f and
A6: for i being Nat st i in D holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) by A2, Th15;
take L ; :: thesis: ( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
thus Sum L = (Mx2Tran M) . f by A5; :: thesis: for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k
let i be Nat; :: thesis: ( i in dom f implies L . (Line (M,i)) = f . i )
assume A7: i in dom f ; :: thesis: L . (Line (M,i)) = f . i
i >= 1 by A7, FINSEQ_3:25;
then A8: Sgm {i} = <*i*> by FINSEQ_3:44;
set LM = Line (M,i);
A9: Line (M,i) in {(Line (M,i))} by TARSKI:def 1;
dom M = Seg n by A3, FINSEQ_1:def 3;
then Line (M,i) in lines M by A4, A7, MATRIX13:103;
then consider x being set such that
A10: M " {(Line (M,i))} = {x} by A2, FUNCT_1:74;
A11: dom (f | {i}) = (dom f) /\ {i} by RELAT_1:61;
{i} c= dom f by A7, ZFMISC_1:31;
then A12: dom (f | {i}) = {i} by A11, XBOOLE_1:28;
then i in dom (f | {i}) by TARSKI:def 1;
then A13: (f | {i}) . i = f . i by FUNCT_1:47;
rng <*i*> = {i} by FINSEQ_1:38;
then A14: <*i*> is FinSequence of {i} by FINSEQ_1:def 4;
( rng (f | {i}) <> {} & f | {i} is Function of {i},(rng (f | {i})) ) by A12, FUNCT_2:1, RELAT_1:42;
then Seq (f | {i}) = <*(f . i)*> by A12, A8, A14, A13, FINSEQ_2:35;
then A15: Sum (Seq (f | {i})) = f . i by RVSUM_1:73;
M . i = Line (M,i) by A4, A7, MATRIX_2:16;
then i in M " {(Line (M,i))} by A4, A7, A9, FUNCT_1:def 7;
then f | (M " {(Line (M,i))}) = f | {i} by A10, TARSKI:def 1;
hence L . (Line (M,i)) = f . i by A6, A4, A7, A15; :: thesis: verum