let n, m be Nat; :: thesis:
let f be n -element real-valued FinSequence; :: thesis:
let M be Matrix of n,m,F_Real; :: thesis:
defpred S₁[ Nat] means for n, m being Nat
for M being Matrix of n,m,F_Real
for f being b₁ -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = $1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) );
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A2: S₁[i] ; :: thesis:
let n, m be Nat; :: thesis:
let M be Matrix of n,m,F_Real; :: thesis:
let f be n -element real-valued FinSequence; :: thesis:
let S be Subset of (Seg n); :: thesis:
assume that
A3: ( n = 0 implies m = 0 ) and
A4: M | S is one-to-one and
A5: rng (M | S) = lines M and
A6: card (lines M) = i + 1 ; :: thesis:
A7: len M = n by A3, MATRIX13:1;
A8: width M = m by A3, MATRIX13:1;

per cases ;

suppose i = 0 ; :: thesis:

then consider L being Linear_Combination of lines M such that
A9: Sum L = (Mx2Tran M) . f and
A10: for i being Nat st i in Seg n holds
( L . (Line (M,i)) = Sum f & M " {(Line (M,i))} = dom f ) by A6, Lm5;
take L ; :: thesis:
thus Sum L = (Mx2Tran M) . f by A9; :: thesis:
let w be Nat; :: thesis:
assume A11: w in S ; :: thesis:
M " {(Line (M,w))} = dom f by A10, A11;
then A12: f | (M " {(Line (M,w))}) = f ;
L . (Line (M,w)) = Sum f by A10, A11;
hence Sum (Seq (f | (M " {(Line (M,w))}))) = L . (Line (M,w)) by A12, FINSEQ_3:116; :: thesis:

end;

suppose A13: i > 0 ; :: thesis:

lines M <> {} by A6;
then consider x being object such that
A14: x in lines M by XBOOLE_0:def 1;
reconsider LM = {x} as Subset of (lines M) by A14, ZFMISC_1:31;
set n1 = n -' (card (M " LM));
reconsider ML1 = M - LM as Matrix of n -' (card (M " LM)),m,F_Real by MATRTOP1:14;
A15: LM ` = (lines M) \ LM by SUBSET_1:def 4;
then A16: LM misses LM ` by XBOOLE_1:79;
LM \/ (LM `) = [#] (lines M) by SUBSET_1:10
.= lines M by SUBSET_1:def 3 ;
then A17: (M " LM) \/ (M " (LM `)) = M " (rng M) by RELAT_1:140
.= dom M by RELAT_1:134 ;
A18: len ML1 = (len M) - (card (M " LM)) by FINSEQ_3:59;
then A19: n - (card (M " LM)) = n -' (card (M " LM)) by A7, XREAL_1:49, XREAL_1:233;
LM misses LM ` by A15, XBOOLE_1:79;
then A20: (card (M " LM)) + (card (M " (LM `))) = card (dom M) by A17, CARD_2:40, FUNCT_1:71
.= n by A7, CARD_1:62 ;
A21: n -' (card (M " LM)) <> 0

proof

assume n -' (card (M " LM)) = 0 ; :: thesis:
then M " (LM `) = {} by A7, A18, A20, XREAL_1:49, XREAL_1:233;
then LM ` misses rng M by RELAT_1:138;
then {} = (lines M) \ LM by A15, XBOOLE_1:67;
then lines M c= LM by XBOOLE_1:37;
then lines M = LM ;
then i + 1 = 1 by A6, CARD_2:42;
hence contradiction by A13; :: thesis:

end;

set n2 = n -' (card (M " (LM `)));
reconsider ML2 = M - (LM `) as Matrix of n -' (card (M " (LM `))),m,F_Real by MATRTOP1:14;
rng ML2 = (rng M) \ (LM `) by FINSEQ_3:65;
then A22: rng ML2 = (LM `) ` by SUBSET_1:def 4;
reconsider FR = F_Real as Field ;
set Mf = (Mx2Tran M) . f;
set V = m -VectSp_over F_Real;
len f = n by CARD_1:def 7;
then A23: dom f = Seg n by FINSEQ_1:def 3;
consider j being object such that
A24: j in dom (M | S) and
A25: (M | S) . j = x by A5, A14, FUNCT_1:def 3;
A26: x = M . j by A24, A25, FUNCT_1:47;
A27: j in dom M by A24, RELAT_1:57;
A28: j in S by A24;
reconsider j = j as Nat by A24;
A29: x = Line (M,j) by A27, A26, MATRIX_0:60;
A30: len ML2 = (len M) - (card (M " (LM `))) by FINSEQ_3:59;
then A31: n - (card (M " (LM `))) = n -' (card (M " (LM `))) by A7, XREAL_1:49, XREAL_1:233;
A32: rng ML1 = (rng M) \ LM by FINSEQ_3:65;
then A33: rng ML1 = LM ` by SUBSET_1:def 4;
reconsider LMj = Line (M,j) as Element of (m -VectSp_over F_Real) by A8, MATRIX13:102;
A34: card (rng ML1) = (card (rng M)) - (card LM) by A32, CARD_2:44
.= (i + 1) - 1 by A6, CARD_2:42 ;
(LM `) ` = LM ;
then consider P being Permutation of (dom M) such that
A35: (M - LM) ^ (M - (LM `)) = M * P by FINSEQ_3:115;
dom M = Seg n by A7, FINSEQ_1:def 3;
then reconsider p = P as Permutation of (Seg n) ;
A36: (M | S) * P = (M | S) * (p | (dom p))
.= (M * p) | ((dom p) /\ (p " S)) by FUNCT_1:100
.= (M * p) | (p " S) by RELAT_1:132, XBOOLE_1:28 ;
reconsider pp = P as one-to-one Function ;
len (M * p) = n by MATRIX_0:def 2;
then A37: dom (M * p) = Seg n by FINSEQ_1:def 3;
set ppj = (pp ") . j;
A38: rng p = Seg n by FUNCT_2:def 3;
then A39: ( p " S = (pp ") .: S & dom (pp ") = Seg n ) by FUNCT_1:33, FUNCT_1:85;
then A40: (pp ") . j in p " S by A28, FUNCT_1:def 6;
A41: p . ((pp ") . j) = j by A28, A38, FUNCT_1:35;
A42: not (pp ") . j in dom ML1

proof

assume A43: (pp ") . j in dom ML1 ; :: thesis:
(M * P) . ((pp ") . j) = M . j by A40, A41, A37, FUNCT_1:12;
then (M * P) . ((pp ") . j) = LMj by A27, MATRIX_0:60;
then ML1 . ((pp ") . j) = LMj by A35, A43, FINSEQ_1:def 7;
then A44: ML1 . ((pp ") . j) in LM by A29, TARSKI:def 1;
ML1 . ((pp ") . j) in LM ` by A33, A43, FUNCT_1:def 3;
hence contradiction by A16, A44, XBOOLE_0:3; :: thesis:

end;

set pSj = (p " S) \ {((pp ") . j)};
dom M = Seg n by A7, FINSEQ_1:def 3;
then A45: dom (M | S) = S by RELAT_1:62;
A46: (p " S) \ {((pp ") . j)} c= dom ML1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A47: y in (p " S) \ {((pp ") . j)} ; :: thesis:
then reconsider Y = y as Nat ;
A48: (M * p) . y = M . (p . y) by A37, A47, FUNCT_1:12;
not y in {((pp ") . j)} by A47, XBOOLE_0:def 5;
then A49: y <> (pp ") . j by TARSKI:def 1;
A50: (pp ") . j in dom P by A40, FUNCT_1:def 7;
A51: y in p " S by A47, XBOOLE_0:def 5;
then A52: p . y in dom (M | S) by A45, FUNCT_1:def 7;
y in dom P by A51, FUNCT_1:def 7;
then p . y <> j by A41, A49, A50, FUNCT_1:def 4;
then (M | S) . (p . y) <> (M | S) . j by A4, A24, A52, FUNCT_1:def 4;
then (M * p) . y <> LMj by A25, A29, A48, A52, FUNCT_1:47;
then A53: not (M * p) . y in LM by A29, TARSKI:def 1;
assume not y in dom ML1 ; :: thesis:
then consider w being Nat such that
A54: w in dom ML2 and
A55: Y = (len ML1) + w by A35, A37, A47, FINSEQ_1:25;
(M * p) . Y = ML2 . w by A35, A54, A55, FINSEQ_1:def 7;
hence contradiction by A22, A53, A54, FUNCT_1:def 3; :: thesis:

end;

then ( (M * p) | ((p " S) \ {((pp ") . j)}) = ((M * p) | (p " S)) | ((p " S) \ {((pp ") . j)}) & (M * p) | ((p " S) \ {((pp ") . j)}) = ML1 | ((p " S) \ {((pp ") . j)}) ) by A35, FINSEQ_6:11, RELAT_1:74, XBOOLE_1:36;
then A56: ML1 | ((p " S) \ {((pp ") . j)}) is one-to-one by A4, A36, FUNCT_1:52;
( dom p = Seg n & p . ((pp ") . j) = j ) by A28, A38, FUNCT_1:35, FUNCT_2:52;
then A57: (pp ") . j in dom ((M | S) * p) by A24, A40, FUNCT_1:11;
then ((M | S) * p) . ((pp ") . j) = LMj by A25, A29, A41, FUNCT_1:12;
then A58: LM = Im (((M | S) * p),((pp ") . j)) by A29, A57, FUNCT_1:59
.= ((M * p) | (p " S)) .: {((pp ") . j)} by A36, RELAT_1:def 16 ;
rng M = rng ((M * p) | (p " S)) by A5, A36, A38, A45, RELAT_1:28
.= (M * p) .: (p " S) by RELAT_1:115
.= ((M * p) | (p " S)) .: (p " S) by RELAT_1:129 ;
then A59: rng ML1 = ((M * p) | (p " S)) .: ((p " S) \ {((pp ") . j)}) by A4, A36, A32, A58, FUNCT_1:64
.= rng (((M * p) | (p " S)) | ((p " S) \ {((pp ") . j)})) by RELAT_1:115
.= rng ((M * p) | ((p " S) \ {((pp ") . j)})) by RELAT_1:74, XBOOLE_1:36
.= rng (ML1 | ((p " S) \ {((pp ") . j)})) by A35, A46, FINSEQ_6:11 ;
reconsider fp = f * p as n -element FinSequence of REAL by MATRTOP1:21;
A60: (n -' (card (M " LM))) + (n -' (card (M " (LM `)))) = len (ML1 ^ ML2) by MATRIX_0:def 2
.= len (M * p) by A35
.= n by MATRIX_0:def 2 ;
len fp = n by CARD_1:def 7;
then consider fp1, fp2 being FinSequence of REAL such that
A61: len fp1 = n -' (card (M " LM)) and
A62: len fp2 = n -' (card (M " (LM `))) and
A63: fp = fp1 ^ fp2 by A60, FINSEQ_2:23;
A64: fp2 is n -' (card (M " (LM `))) -element by A62, CARD_1:def 7;
then A65: len ((Mx2Tran ML2) . fp2) = m by CARD_1:def 7;
card LM = 1 by CARD_2:42;
then consider L2 being Linear_Combination of lines ML2 such that
A66: Sum L2 = (Mx2Tran ML2) . fp2 and
A67: for i being Nat st i in Seg (n -' (card (M " (LM `)))) holds
( L2 . (Line (ML2,i)) = Sum fp2 & ML2 " {(Line (ML2,i))} = dom fp2 ) by A64, A22, Lm5;
A68: fp1 is n -' (card (M " LM)) -element by A61, CARD_1:def 7;
then len ((Mx2Tran ML1) . fp1) = m by CARD_1:def 7;
then reconsider Mf1 = @ ((Mx2Tran ML1) . fp1), Mf2 = @ ((Mx2Tran ML2) . fp2) as Element of m -tuples_on the carrier of F_Real by A65, FINSEQ_2:92;
A69: Carrier L2 c= lines ML2 by VECTSP_6:def 4;
len ML1 = n -' (card (M " LM)) by A7, A18, XREAL_1:49, XREAL_1:233;
then (p " S) \ {((pp ") . j)} is Subset of (Seg (n -' (card (M " LM)))) by A46, FINSEQ_1:def 3;
then consider L1 being Linear_Combination of lines ML1 such that
A70: Sum L1 = (Mx2Tran ML1) . fp1 and
A71: for i being Nat st i in (p " S) \ {((pp ") . j)} holds
L1 . (Line (ML1,i)) = Sum (Seq (fp1 | (ML1 " {(Line (ML1,i))}))) by A2, A68, A21, A56, A59, A34;
A72: Carrier L1 c= lines ML1 by VECTSP_6:def 4;
(rng ML1) \/ (rng ML2) = [#] (lines M) by A22, A33, SUBSET_1:10
.= lines M by SUBSET_1:def 3 ;
then ( L1 is Linear_Combination of lines M & L2 is Linear_Combination of lines M ) by VECTSP_6:4, XBOOLE_1:7;
then reconsider L12 = L1 + L2 as Linear_Combination of lines M by VECTSP_6:24;
take L12 ; :: thesis:
thus (Mx2Tran M) . f = (Mx2Tran (ML1 ^ ML2)) . (fp1 ^ fp2) by A35, A60, A63, MATRTOP1:21
.= ((Mx2Tran ML1) . fp1) + ((Mx2Tran ML2) . fp2) by A68, A64, MATRTOP1:36
.= Mf1 + Mf2 by MATRTOP1:1
.= (Sum L1) + (Sum L2) by A70, A66, MATRIX13:102
.= Sum L12 by VECTSP_6:44 ; :: thesis:
let w be Nat; :: thesis:
assume A73: w in S ; :: thesis:
Line (M,w) in lines M by A73, MATRIX13:103;
then reconsider LMw = Line (M,w) as Element of (m -VectSp_over F_Real) ;
p " (M " {LMw}) = (M * p) " {LMw} by RELAT_1:146;
then A74: Sum (Seq (f | (M " {LMw}))) = Sum (Seq (fp | ((M * p) " {LMw}))) by A23, MATRTOP1:10
.= Sum ((Seq (fp1 | (ML1 " {LMw}))) ^ (Seq (fp2 | (ML2 " {LMw})))) by A7, A35, A61, A62, A63, A18, A30, A19, A31, MATRTOP1:13
.= (Sum (Seq (fp1 | (ML1 " {LMw})))) + (Sum (Seq (fp2 | (ML2 " {LMw})))) by RVSUM_1:75 ;
set ppw = (pp ") . w;
A75: (pp ") . w in p " S by A39, A73, FUNCT_1:def 6;
p . ((pp ") . w) = w by A38, A73, FUNCT_1:35;
then A76: (M * P) . ((pp ") . w) = M . w by A37, A75, FUNCT_1:12;
reconsider ppw = (pp ") . w as Nat by A75;
A77: M . w = LMw by A73, MATRIX_0:52;
reconsider L1w = L1 . LMw, L2w = L2 . LMw as Element of FR ;
A78: L12 . LMw = L1w + L2w by VECTSP_6:22;

per cases by A35, A37, A75, FINSEQ_1:25;

suppose A79: ppw in dom ML1 ; :: thesis:

then A80: ML1 . ppw = LMw by A35, A76, A77, FINSEQ_1:def 7;
then A81: LMw in rng ML1 by A79, FUNCT_1:def 3;
then not LMw in Carrier L2 by A22, A33, A69, A16, XBOOLE_0:3;
then A82: L2 . LMw = 0. F_Real by VECTSP_6:2;
not LMw in rng ML2 by A22, A33, A16, A81, XBOOLE_0:3;
then {LMw} misses rng ML2 by ZFMISC_1:50;
then ML2 " {LMw} = {} by RELAT_1:138;
then A83: Sum (Seq (fp2 | (ML2 " {LMw}))) = 0 by RVSUM_1:72;
( Line (ML1,ppw) = ML1 . ppw & ppw in (p " S) \ {((pp ") . j)} ) by A75, A42, A79, MATRIX_0:60, ZFMISC_1:56;
then L1 . LMw = Sum (Seq (fp1 | (ML1 " {LMw}))) by A71, A80;
hence L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) by A74, A78, A82, A83, RLVECT_1:def 4; :: thesis:

end;

suppose ex z being Nat st
( z in dom ML2 & ppw = (len ML1) + z ) ; :: thesis:

then consider z being Nat such that
A84: z in dom ML2 and
A85: ppw = (len ML1) + z ;
A86: ML2 . z = LMw by A35, A76, A77, A84, A85, FINSEQ_1:def 7;
then A87: LMw in rng ML2 by A84, FUNCT_1:def 3;
then not LMw in Carrier L1 by A22, A33, A72, A16, XBOOLE_0:3;
then A88: L1 . LMw = 0. F_Real by VECTSP_6:2;
not LMw in LM ` by A22, A16, A87, XBOOLE_0:3;
then {LMw} misses rng ML1 by A33, ZFMISC_1:50;
then ML1 " {LMw} = {} by RELAT_1:138;
then A89: Seq (fp1 | (ML1 " {LMw})) = <*> REAL ;
L1w + L2w = L2w + L1w by RLVECT_1:def 2;
then A90: L12 . LMw = L2 . LMw by A78, A88, RLVECT_1:def 4;
A91: dom ML2 = Seg (n -' (card (M " (LM `)))) by A7, A30, A31, FINSEQ_1:def 3;
A92: ML2 . z = Line (ML2,z) by A84, MATRIX_0:60;
then ML2 " {LMw} = dom fp2 by A67, A84, A86, A91;
then A93: fp2 | (ML2 " {LMw}) = fp2 ;
L2 . LMw = Sum fp2 by A67, A84, A86, A92, A91;
hence L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) by A74, A90, A89, A93, FINSEQ_3:116, RVSUM_1:72; :: thesis:

end;

A94: S₁[ 0 ]

proof

let n, m be Nat; :: thesis:
let M be Matrix of n,m,F_Real; :: thesis:
let f be n -element real-valued FinSequence; :: thesis:
let S be Subset of (Seg n); :: thesis:
assume that
A95: ( n = 0 implies m = 0 ) and
M | S is one-to-one and
rng (M | S) = lines M and
A96: card (lines M) = 0 ; :: thesis:
reconsider L = ZeroLC (m -VectSp_over F_Real) as Linear_Combination of lines M by VECTSP_6:5;
take L ; :: thesis:
A97: Sum L = 0. (m -VectSp_over F_Real) by VECTSP_6:15
.= 0. (TOP-REAL m) by Lm2 ;
A98: ( len M = n & M = {} ) by A95, A96, MATRIX13:1;
thus Sum L = (Mx2Tran M) . f by A95, A98, A97; :: thesis:
let i be Nat; :: thesis:
thus ( i in S implies L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) by A98; :: thesis:

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A94, A1);
then A99: S₁[ card (lines M)] ;

per cases ;

suppose n <> 0 ; :: thesis:

hence for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) ) by A99; :: thesis:

end;

suppose A100: n = 0 ; :: thesis:

let S be Subset of (Seg n); :: thesis:
assume ( M | S is one-to-one & rng (M | S) = lines M ) ; :: thesis:
reconsider L = ZeroLC (m -VectSp_over F_Real) as Linear_Combination of lines M by VECTSP_6:5;
take L ; :: thesis:
thus Sum L = 0. (m -VectSp_over F_Real) by VECTSP_6:15
.= 0. (TOP-REAL m) by Lm2
.= (Mx2Tran M) . f by A100, MATRTOP1:def 3 ; :: thesis:
thus for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) by A100; :: thesis:

end;