let n, m be Nat; 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; 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; ( 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
; 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
; ( 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; for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k
let i be Nat; ( i in dom f implies L . (Line (M,i)) = f . i )
assume A6:
i in dom f
; 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; verum