let m, n 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 by RELAT_1:69;
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 set 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 by XBOOLE_0:def 10;
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 set 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, RELAT_1:57;
reconsider j = j as Nat by A24;
A29: x = Line (M,j) by A27, A26, MATRIX_2:16;
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;
A33: rng ML1 = (rng M) \ LM by FINSEQ_3:65;
then A34: 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;
A35: card (rng ML1) = (card (rng M)) - (card LM) by A33, CARD_2:44
.= (i + 1) - 1 by A6, CARD_2:42 ;
(LM `) ` = LM ;
then consider P being Permutation of (dom M) such that
A36: (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) ;
A37: (M | S) * P = (M | S) * (p | (dom p)) by RELAT_1:69
.= (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_1:def 2;
then A38: dom (M * p) = Seg n by FINSEQ_1:def 3;
set ppj = (pp ") . j;
A39: rng p = Seg n by FUNCT_2:def 3;
then A40: ( p " S = (pp ") .: S & dom (pp ") = Seg n ) by FUNCT_1:33, FUNCT_1:85;
then A41: (pp ") . j in p " S by A28, FUNCT_1:def 6;
A42: p . ((pp ") . j) = j by A28, A39, FUNCT_1:35;
A43: not (pp ") . j in dom ML1

proof

assume A44: (pp ") . j in dom ML1 ; :: thesis:
(M * P) . ((pp ") . j) = M . j by A41, A42, A38, FUNCT_1:12;
then (M * P) . ((pp ") . j) = LMj by A27, MATRIX_2:16;
then ML1 . ((pp ") . j) = LMj by A36, A44, FINSEQ_1:def 7;
then A45: ML1 . ((pp ") . j) in LM by A29, TARSKI:def 1;
ML1 . ((pp ") . j) in LM ` by A34, A44, FUNCT_1:def 3;
hence contradiction by A16, A45, XBOOLE_0:3; :: thesis:

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A48: y in (p " S) \ {((pp ") . j)} ; :: thesis:
then reconsider Y = y as Nat ;
A49: (M * p) . y = M . (p . y) by A38, A48, FUNCT_1:12;
not y in {((pp ") . j)} by A48, XBOOLE_0:def 5;
then A50: y <> (pp ") . j by TARSKI:def 1;
A51: (pp ") . j in dom P by A41, FUNCT_1:def 7;
A52: y in p " S by A48, XBOOLE_0:def 5;
then A53: p . y in dom (M | S) by A46, FUNCT_1:def 7;
y in dom P by A52, FUNCT_1:def 7;
then p . y <> j by A42, A50, A51, FUNCT_1:def 4;
then (M | S) . (p . y) <> (M | S) . j by A4, A24, A53, FUNCT_1:def 4;
then (M * p) . y <> LMj by A25, A29, A49, A53, FUNCT_1:47;
then A54: 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
A55: w in dom ML2 and
A56: Y = (len ML1) + w by A36, A38, A48, FINSEQ_1:25;
(M * p) . Y = ML2 . w by A36, A55, A56, FINSEQ_1:def 7;
hence contradiction by A22, A54, A55, 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 A36, FINSEQ_6:11, RELAT_1:74, XBOOLE_1:36;
then A57: ML1 | ((p " S) \ {((pp ") . j)}) is one-to-one by A4, A37, FUNCT_1:52;
( dom p = Seg n & p . ((pp ") . j) = j ) by A28, A39, FUNCT_1:35, FUNCT_2:52;
then A58: (pp ") . j in dom ((M | S) * p) by A24, A41, FUNCT_1:11;
then ((M | S) * p) . ((pp ") . j) = LMj by A25, A29, A42, FUNCT_1:12;
then A59: LM = Im (((M | S) * p),((pp ") . j)) by A29, A58, FUNCT_1:59
.= ((M * p) | (p " S)) .: {((pp ") . j)} by A37, RELAT_1:def 16 ;
rng M = rng ((M * p) | (p " S)) by A5, A37, A39, A46, RELAT_1:28
.= (M * p) .: (p " S) by RELAT_1:115
.= ((M * p) | (p " S)) .: (p " S) by RELAT_1:129 ;
then A60: rng ML1 = ((M * p) | (p " S)) .: ((p " S) \ {((pp ") . j)}) by A4, A37, A33, A59, 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 A36, A47, FINSEQ_6:11 ;
reconsider fp = f * p as n -element FinSequence of REAL by MATRTOP1:21;
A61: (n -' (card (M " LM))) + (n -' (card (M " (LM `)))) = len (ML1 ^ ML2) by MATRIX_1:def 2
.= len (M * p) by A36
.= n by MATRIX_1:def 2 ;
len fp = n by CARD_1:def 7;
then consider fp1, fp2 being FinSequence of REAL such that
A62: len fp1 = n -' (card (M " LM)) and
A63: len fp2 = n -' (card (M " (LM `))) and
A64: fp = fp1 ^ fp2 by A61, FINSEQ_2:23;
A65: fp2 is n -' (card (M " (LM `))) -element by A63, CARD_1:def 7;
then A66: 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
A67: Sum L2 = (Mx2Tran ML2) . fp2 and
A68: 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 A65, A22, Lm5;
A69: fp1 is n -' (card (M " LM)) -element by A62, 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 A66, FINSEQ_2:92;
A70: 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 A47, FINSEQ_1:def 3;
then consider L1 being Linear_Combination of lines ML1 such that
A71: Sum L1 = (Mx2Tran ML1) . fp1 and
A72: 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, A69, A21, A57, A60, A35;
A73: Carrier L1 c= lines ML1 by VECTSP_6:def 4;
(rng ML1) \/ (rng ML2) = [#] (lines M) by A22, A34, 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 A36, A61, A64, MATRTOP1:21
.= ((Mx2Tran ML1) . fp1) + ((Mx2Tran ML2) . fp2) by A69, A65, MATRTOP1:36
.= Mf1 + Mf2 by MATRTOP1:1
.= (Sum L1) + (Sum L2) by A71, A67, MATRIX13:102
.= Sum L12 by VECTSP_6:44 ; :: thesis:
let w be Nat; :: thesis:
assume A74: w in S ; :: thesis:
Line (M,w) in lines M by A74, 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 A75: 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, A36, A62, A63, A64, A18, A30, A19, A31, MATRTOP1:13
.= (Sum (Seq (fp1 | (ML1 " {LMw})))) + (Sum (Seq (fp2 | (ML2 " {LMw})))) by RVSUM_1:75 ;
set ppw = (pp ") . w;
A76: (pp ") . w in p " S by A40, A74, FUNCT_1:def 6;
p . ((pp ") . w) = w by A39, A74, FUNCT_1:35;
then A77: (M * P) . ((pp ") . w) = M . w by A38, A76, FUNCT_1:12;
reconsider ppw = (pp ") . w as Nat by A76;
A78: M . w = LMw by A74, MATRIX_2:8;
reconsider L1w = L1 . LMw, L2w = L2 . LMw as Element of FR ;
A79: L12 . LMw = L1w + L2w by VECTSP_6:22;

per cases by A36, A38, A76, FINSEQ_1:25;

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

then A81: ML1 . ppw = LMw by A36, A77, A78, FINSEQ_1:def 7;
then A82: LMw in rng ML1 by A80, FUNCT_1:def 3;
then not LMw in Carrier L2 by A22, A34, A70, A16, XBOOLE_0:3;
then A83: L2 . LMw = 0. F_Real by VECTSP_6:2;
not LMw in rng ML2 by A22, A34, A16, A82, XBOOLE_0:3;
then {LMw} misses rng ML2 by ZFMISC_1:50;
then ML2 " {LMw} = {} by RELAT_1:138;
then A84: Sum (Seq (fp2 | (ML2 " {LMw}))) = 0 by RVSUM_1:72;
( Line (ML1,ppw) = ML1 . ppw & ppw in (p " S) \ {((pp ") . j)} ) by A76, A43, A80, MATRIX_2:16, ZFMISC_1:56;
then L1 . LMw = Sum (Seq (fp1 | (ML1 " {LMw}))) by A72, A81;
hence L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) by A75, A79, A83, A84, 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
A85: z in dom ML2 and
A86: ppw = (len ML1) + z ;
A87: ML2 . z = LMw by A36, A77, A78, A85, A86, FINSEQ_1:def 7;
then A88: LMw in rng ML2 by A85, FUNCT_1:def 3;
then not LMw in Carrier L1 by A22, A34, A73, A16, XBOOLE_0:3;
then A89: L1 . LMw = 0. F_Real by VECTSP_6:2;
not LMw in LM ` by A22, A16, A88, XBOOLE_0:3;
then {LMw} misses rng ML1 by A34, ZFMISC_1:50;
then ML1 " {LMw} = {} by RELAT_1:138;
then A90: Seq (fp1 | (ML1 " {LMw})) = <*> REAL ;
L1w + L2w = L2w + L1w by RLVECT_1:def 2;
then A91: L12 . LMw = L2 . LMw by A79, A89, RLVECT_1:def 4;
A92: dom ML2 = Seg (n -' (card (M " (LM `)))) by A7, A30, A31, FINSEQ_1:def 3;
A93: ML2 . z = Line (ML2,z) by A85, MATRIX_2:16;
then ML2 " {LMw} = dom fp2 by A68, A85, A87, A92;
then A94: fp2 | (ML2 " {LMw}) = fp2 by RELAT_1:69;
L2 . LMw = Sum fp2 by A68, A85, A87, A93, A92;
hence L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) by A75, A91, A90, A94, FINSEQ_3:116, RVSUM_1:72; :: thesis:

end;

A95: 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
A96: ( n = 0 implies m = 0 ) and
M | S is one-to-one and
rng (M | S) = lines M and
A97: 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:
A98: Sum L = 0. (m -VectSp_over F_Real) by VECTSP_6:15
.= 0. (TOP-REAL m) by Lm2 ;
A99: ( len M = n & M = {} ) by A96, A97, MATRIX13:1;
then 0. (TOP-REAL m) = {} by A96;
hence Sum L = (Mx2Tran M) . f by A96, A99, A98; :: thesis:
let i be Nat; :: thesis:
thus ( i in S implies L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) by A99; :: thesis:

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A95, A1);
then A100: 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 A100; :: thesis:

end;

suppose B1: 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 B1, 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 B1; :: thesis:

end;