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 without_repeated_line 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 without_repeated_line 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 without_repeated_line 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 A1: M is without_repeated_line ; :: 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 ) )
A2: len M = n by MATRIX_0: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 A3: dom f = dom M by A2, FINSEQ_3:29;
M | (dom M) = M ;
then consider L being Linear_Combination of lines M such that
A4: Sum L = (Mx2Tran M) . f and
A5: for i being Nat st i in D holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) by A1, 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 A4; :: 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 A6: i in dom f ; :: thesis: L . (Line (M,i)) = f . i
i >= 1 by A6, FINSEQ_3:25;
then A7: Sgm {i} = <*i*> by FINSEQ_3:44;
set LM = Line (M,i);
A8: Line (M,i) in {(Line (M,i))} by TARSKI:def 1;
dom M = Seg n by A2, FINSEQ_1:def 3;
then Line (M,i) in lines M by A3, A6, MATRIX13:103;
then consider x being object such that
A9: M " {(Line (M,i))} = {x} by A1, FUNCT_1:74;
A10: dom (f | {i}) = (dom f) /\ {i} by RELAT_1:61;
{i} c= dom f by A6, ZFMISC_1:31;
then A11: dom (f | {i}) = {i} by A10, XBOOLE_1:28;
then i in dom (f | {i}) by TARSKI:def 1;
then A12: (f | {i}) . i = f . i by FUNCT_1:47;
rng <*i*> = {i} by FINSEQ_1:38;
then A13: <*i*> is FinSequence of {i} by FINSEQ_1:def 4;
( rng (f | {i}) <> {} & f | {i} is Function of {i},(rng (f | {i})) ) by A11, FUNCT_2:1, RELAT_1:42;
then Seq (f | {i}) = <*(f . i)*> by A11, A7, A13, A12, FINSEQ_2:35;
then A14: Sum (Seq (f | {i})) = f . i by RVSUM_1:73;
M . i = Line (M,i) by A3, A6, MATRIX_0:60;
then i in M " {(Line (M,i))} by A3, A6, A8, FUNCT_1:def 7;
then f | (M " {(Line (M,i))}) = f | {i} by A9, TARSKI:def 1;
hence L . (Line (M,i)) = f . i by A5, A3, A6, A14; :: thesis: verum