let m, n be Nat; :: thesis: for K being Field

for A being Matrix of n,m,K

for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

let K be Field; :: thesis: for A being Matrix of n,m,K

for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

let A be Matrix of n,m,K; :: thesis: for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

let N be finite without_zero Subset of NAT; :: thesis: ( card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 implies ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) ) )

assume that

A1: card N = n and

A2: N c= Seg m and

A3: Segm (A,(Seg n),N) = 1. (K,n) and

A4: n > 0 ; :: thesis: ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

set SN = (Seg m) \ N;

A5: ( m -' n = 0 or m -' n > 0 ) ;

A6: card (Seg m) = m by FINSEQ_1:57;

then A7: card ((Seg m) \ N) = m - n by A1, A2, CARD_2:44;

set ZERO = 0. (K,(m -' n),m);

A8: (Seg m) \ N c= Seg m by XBOOLE_1:36;

card (Seg n) = n by FINSEQ_1:57;

then A10: len (Segm (A,(Seg n),((Seg m) \ N))) = n by A4, MATRIX_0:23;

A11: ( len ((Segm (A,(Seg n),((Seg m) \ N))) @) = len (- ((Segm (A,(Seg n),((Seg m) \ N))) @)) & width ((Segm (A,(Seg n),((Seg m) \ N))) @) = width (- ((Segm (A,(Seg n),((Seg m) \ N))) @)) ) by MATRIX_3:def 2;

A12: width A = m by A4, MATRIX_0:23;

Segm n c= Segm (card (Seg m)) by A1, A2, CARD_1:11;

then A13: n <= m by A6, NAT_1:39;

then A14: m -' n = m - n by XREAL_1:233;

then width (Segm (A,(Seg n),((Seg m) \ N))) = m -' n by A4, A7, MATRIX_0:23;

then ( ( len ((Segm (A,(Seg n),((Seg m) \ N))) @) = 0 & m -' n = 0 ) or ( len ((Segm (A,(Seg n),((Seg m) \ N))) @) = m -' n & width ((Segm (A,(Seg n),((Seg m) \ N))) @) = n ) ) by A10, A5, MATRIX_0:54, MATRIX_0:def 6;

then ( ( - ((Segm (A,(Seg n),((Seg m) \ N))) @) = {} & m -' n = 0 ) or - ((Segm (A,(Seg n),((Seg m) \ N))) @) is Matrix of m -' n,n,K ) by A11, MATRIX_0:51;

then reconsider SAT = - ((Segm (A,(Seg n),((Seg m) \ N))) @) as Matrix of m -' n,n,K by MATRIX_0:13;

set ONE = 1. (K,(m -' n));

A15: N misses (Seg m) \ N by XBOOLE_1:79;

[:(Seg (m -' n)),N:] /\ [:(Seg (m -' n)),((Seg m) \ N):] = [:(Seg (m -' n)),(N /\ ((Seg m) \ N)):] by ZFMISC_1:99

.= [:(Seg (m -' n)),{}:] by A15

.= {} by ZFMISC_1:90 ;

then ( card (Seg (m -' n)) = m -' n & ( for i, j, bi, bj, ci, cj being Nat st [i,j] in [:(Seg (m -' n)),N:] /\ [:(Seg (m -' n)),((Seg m) \ N):] & bi = ((Sgm (Seg (m -' n))) ") . i & bj = ((Sgm N) ") . j & ci = ((Sgm (Seg (m -' n))) ") . i & cj = ((Sgm ((Seg m) \ N)) ") . j holds

SAT * (bi,bj) = (1. (K,(m -' n))) * (ci,cj) ) ) by FINSEQ_1:57;

then consider V being Matrix of len (0. (K,(m -' n),m)), width (0. (K,(m -' n),m)),K such that

A16: Segm (V,(Seg (m -' n)),N) = SAT and

A17: Segm (V,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) and

for i, j being Nat st [i,j] in (Indices V) \ ([:(Seg (m -' n)),N:] \/ [:(Seg (m -' n)),((Seg m) \ N):]) holds

V * (i,j) = (0. (K,(m -' n),m)) * (i,j) by A1, A9, A14, A7, Th9;

( m -' n = 0 or m -' n > 0 ) ;

then ( ( len (0. (K,(m -' n),m)) = 0 & m -' n = 0 & len V = len (0. (K,(m -' n),m)) ) or ( len (0. (K,(m -' n),m)) = m -' n & width (0. (K,(m -' n),m)) = m ) ) by MATRIX_0:23, MATRIX_0:def 2;

then ( ( V = {} & m -' n = 0 ) or V is Matrix of m -' n,m,K ) ;

then reconsider V = V as Matrix of m -' n,m,K ;

take V ; :: thesis: ( Segm (V,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (V,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

thus ( Segm (V,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (V,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) ) by A16, A17; :: thesis: for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l)))

let l be Nat; :: thesis: for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l)))

let M be Matrix of m,l,K; :: thesis: ( ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ) implies M in Solutions_of (A,(0. (K,n,l))) )

assume A18: for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ; :: thesis: M in Solutions_of (A,(0. (K,n,l)))

set Z = 0. (K,n,l);

A19: len M = m by A4, A13, MATRIX_0:23;

A20: width M = l by A4, A13, MATRIX_0:23;

then A21: width (A * M) = l by A12, A19, MATRIX_3:def 4;

len A = n by A4, MATRIX_0:23;

then len (A * M) = n by A12, A19, MATRIX_3:def 4;

then reconsider AM = A * M as Matrix of n,l,K by A21, MATRIX_0:51;

A22: Indices A = [:(Seg n),(Seg m):] by A4, MATRIX_0:23;

then A23: [:(Seg n),N:] c= Indices A by A2, ZFMISC_1:96;

hence M in Solutions_of (A,(0. (K,n,l))) by A12, A19, A20, A21; :: thesis: verum

for A being Matrix of n,m,K

for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

let K be Field; :: thesis: for A being Matrix of n,m,K

for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

let A be Matrix of n,m,K; :: thesis: for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 holds

ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

let N be finite without_zero Subset of NAT; :: thesis: ( card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 implies ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) ) )

assume that

A1: card N = n and

A2: N c= Seg m and

A3: Segm (A,(Seg n),N) = 1. (K,n) and

A4: n > 0 ; :: thesis: ex MVectors being Matrix of m -' n,m,K st

( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

set SN = (Seg m) \ N;

A5: ( m -' n = 0 or m -' n > 0 ) ;

A6: card (Seg m) = m by FINSEQ_1:57;

then A7: card ((Seg m) \ N) = m - n by A1, A2, CARD_2:44;

set ZERO = 0. (K,(m -' n),m);

A8: (Seg m) \ N c= Seg m by XBOOLE_1:36;

A9: now :: thesis: ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) )end;

set SA = Segm (A,(Seg n),((Seg m) \ N));per cases
( m -' n = 0 or m -' n > 0 )
;

end;

suppose
m -' n = 0
; :: thesis: ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) )

then
Seg (m -' n) = {}
;

then ( [:(Seg (m -' n)),N:] = {} & [:(Seg (m -' n)),((Seg m) \ N):] = {} ) by ZFMISC_1:90;

hence ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) ) ; :: thesis: verum

end;then ( [:(Seg (m -' n)),N:] = {} & [:(Seg (m -' n)),((Seg m) \ N):] = {} ) by ZFMISC_1:90;

hence ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) ) ; :: thesis: verum

suppose
m -' n > 0
; :: thesis: ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) )

then
Indices (0. (K,(m -' n),m)) = [:(Seg (m -' n)),(Seg m):]
by MATRIX_0:23;

hence ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) ) by A2, A8, ZFMISC_1:96; :: thesis: verum

end;hence ( [:(Seg (m -' n)),N:] c= Indices (0. (K,(m -' n),m)) & [:(Seg (m -' n)),((Seg m) \ N):] c= Indices (0. (K,(m -' n),m)) ) by A2, A8, ZFMISC_1:96; :: thesis: verum

card (Seg n) = n by FINSEQ_1:57;

then A10: len (Segm (A,(Seg n),((Seg m) \ N))) = n by A4, MATRIX_0:23;

A11: ( len ((Segm (A,(Seg n),((Seg m) \ N))) @) = len (- ((Segm (A,(Seg n),((Seg m) \ N))) @)) & width ((Segm (A,(Seg n),((Seg m) \ N))) @) = width (- ((Segm (A,(Seg n),((Seg m) \ N))) @)) ) by MATRIX_3:def 2;

A12: width A = m by A4, MATRIX_0:23;

Segm n c= Segm (card (Seg m)) by A1, A2, CARD_1:11;

then A13: n <= m by A6, NAT_1:39;

then A14: m -' n = m - n by XREAL_1:233;

then width (Segm (A,(Seg n),((Seg m) \ N))) = m -' n by A4, A7, MATRIX_0:23;

then ( ( len ((Segm (A,(Seg n),((Seg m) \ N))) @) = 0 & m -' n = 0 ) or ( len ((Segm (A,(Seg n),((Seg m) \ N))) @) = m -' n & width ((Segm (A,(Seg n),((Seg m) \ N))) @) = n ) ) by A10, A5, MATRIX_0:54, MATRIX_0:def 6;

then ( ( - ((Segm (A,(Seg n),((Seg m) \ N))) @) = {} & m -' n = 0 ) or - ((Segm (A,(Seg n),((Seg m) \ N))) @) is Matrix of m -' n,n,K ) by A11, MATRIX_0:51;

then reconsider SAT = - ((Segm (A,(Seg n),((Seg m) \ N))) @) as Matrix of m -' n,n,K by MATRIX_0:13;

set ONE = 1. (K,(m -' n));

A15: N misses (Seg m) \ N by XBOOLE_1:79;

[:(Seg (m -' n)),N:] /\ [:(Seg (m -' n)),((Seg m) \ N):] = [:(Seg (m -' n)),(N /\ ((Seg m) \ N)):] by ZFMISC_1:99

.= [:(Seg (m -' n)),{}:] by A15

.= {} by ZFMISC_1:90 ;

then ( card (Seg (m -' n)) = m -' n & ( for i, j, bi, bj, ci, cj being Nat st [i,j] in [:(Seg (m -' n)),N:] /\ [:(Seg (m -' n)),((Seg m) \ N):] & bi = ((Sgm (Seg (m -' n))) ") . i & bj = ((Sgm N) ") . j & ci = ((Sgm (Seg (m -' n))) ") . i & cj = ((Sgm ((Seg m) \ N)) ") . j holds

SAT * (bi,bj) = (1. (K,(m -' n))) * (ci,cj) ) ) by FINSEQ_1:57;

then consider V being Matrix of len (0. (K,(m -' n),m)), width (0. (K,(m -' n),m)),K such that

A16: Segm (V,(Seg (m -' n)),N) = SAT and

A17: Segm (V,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) and

for i, j being Nat st [i,j] in (Indices V) \ ([:(Seg (m -' n)),N:] \/ [:(Seg (m -' n)),((Seg m) \ N):]) holds

V * (i,j) = (0. (K,(m -' n),m)) * (i,j) by A1, A9, A14, A7, Th9;

( m -' n = 0 or m -' n > 0 ) ;

then ( ( len (0. (K,(m -' n),m)) = 0 & m -' n = 0 & len V = len (0. (K,(m -' n),m)) ) or ( len (0. (K,(m -' n),m)) = m -' n & width (0. (K,(m -' n),m)) = m ) ) by MATRIX_0:23, MATRIX_0:def 2;

then ( ( V = {} & m -' n = 0 ) or V is Matrix of m -' n,m,K ) ;

then reconsider V = V as Matrix of m -' n,m,K ;

take V ; :: thesis: ( Segm (V,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (V,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & ( for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l))) ) )

thus ( Segm (V,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (V,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) ) by A16, A17; :: thesis: for l being Nat

for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l)))

let l be Nat; :: thesis: for M being Matrix of m,l,K st ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ) holds

M in Solutions_of (A,(0. (K,n,l)))

let M be Matrix of m,l,K; :: thesis: ( ( for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ) implies M in Solutions_of (A,(0. (K,n,l))) )

assume A18: for i being Nat holds

( not i in Seg l or ex j being Nat st

( j in Seg (m -' n) & Col (M,i) = Line (V,j) ) or Col (M,i) = m |-> (0. K) ) ; :: thesis: M in Solutions_of (A,(0. (K,n,l)))

set Z = 0. (K,n,l);

A19: len M = m by A4, A13, MATRIX_0:23;

A20: width M = l by A4, A13, MATRIX_0:23;

then A21: width (A * M) = l by A12, A19, MATRIX_3:def 4;

len A = n by A4, MATRIX_0:23;

then len (A * M) = n by A12, A19, MATRIX_3:def 4;

then reconsider AM = A * M as Matrix of n,l,K by A21, MATRIX_0:51;

A22: Indices A = [:(Seg n),(Seg m):] by A4, MATRIX_0:23;

then A23: [:(Seg n),N:] c= Indices A by A2, ZFMISC_1:96;

now :: thesis: for i, j being Nat st [i,j] in Indices AM holds

AM * (i,j) = (0. (K,n,l)) * (i,j)

then
AM = 0. (K,n,l)
by MATRIX_0:27;AM * (i,j) = (0. (K,n,l)) * (i,j)

A24:
Indices AM = Indices (0. (K,n,l))
by MATRIX_0:26;

let i, j be Nat; :: thesis: ( [i,j] in Indices AM implies AM * (i,j) = (0. (K,n,l)) * (i,j) )

assume A25: [i,j] in Indices AM ; :: thesis: AM * (i,j) = (0. (K,n,l)) * (i,j)

reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;

A26: Indices AM = [:(Seg n),(Seg l):] by A4, MATRIX_0:23;

then A27: I in Seg n by A25, ZFMISC_1:87;

A28: J in Seg l by A25, A26, ZFMISC_1:87;

end;let i, j be Nat; :: thesis: ( [i,j] in Indices AM implies AM * (i,j) = (0. (K,n,l)) * (i,j) )

assume A25: [i,j] in Indices AM ; :: thesis: AM * (i,j) = (0. (K,n,l)) * (i,j)

reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;

A26: Indices AM = [:(Seg n),(Seg l):] by A4, MATRIX_0:23;

then A27: I in Seg n by A25, ZFMISC_1:87;

A28: J in Seg l by A25, A26, ZFMISC_1:87;

now :: thesis: (0. (K,n,l)) * (i,j) = AM * (i,j)end;

hence
AM * (i,j) = (0. (K,n,l)) * (i,j)
; :: thesis: verumper cases
( ex jj being Nat st

( jj in Seg (m -' n) & Col (M,J) = Line (V,jj) ) or Col (M,J) = m |-> (0. K) ) by A18, A28;

end;

( jj in Seg (m -' n) & Col (M,J) = Line (V,jj) ) or Col (M,J) = m |-> (0. K) ) by A18, A28;

suppose
ex jj being Nat st

( jj in Seg (m -' n) & Col (M,J) = Line (V,jj) ) ; :: thesis: (0. (K,n,l)) * (i,j) = AM * (i,j)

( jj in Seg (m -' n) & Col (M,J) = Line (V,jj) ) ; :: thesis: (0. (K,n,l)) * (i,j) = AM * (i,j)

then consider jj being Nat such that

A29: jj in Seg (m -' n) and

A30: Col (M,J) = Line (V,jj) ;

A31: jj = (idseq (m -' n)) . jj by A29, FINSEQ_2:49

.= (Sgm (Seg (m -' n))) . jj by FINSEQ_3:48 ;

A32: Indices (1. (K,(m -' n))) = [:(Seg (m -' n)),(Seg (m -' n)):] by MATRIX_0:24;

then A33: [jj,jj] in Indices (1. (K,(m -' n))) by A29, ZFMISC_1:87;

A34: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by A8, FINSEQ_1:def 13;

A35: dom (Sgm ((Seg m) \ N)) = Seg (m -' n) by A14, A7, FINSEQ_3:40, XBOOLE_1:36;

then A36: (Sgm ((Seg m) \ N)) . jj in (Seg m) \ N by A29, A34, FUNCT_1:def 3;

then A37: (Line (A,I)) . ((Sgm ((Seg m) \ N)) . jj) = A * (I,((Sgm ((Seg m) \ N)) . jj)) by A12, A8, MATRIX_0:def 7;

A38: m -' n <> 0 by A29;

then A39: width V = m by MATRIX_0:23;

then A40: (Line (V,jj)) . ((Sgm ((Seg m) \ N)) . jj) = V * (jj,((Sgm ((Seg m) \ N)) . jj)) by A8, A36, MATRIX_0:def 7

.= (1. (K,(m -' n))) * (jj,jj) by A17, A31, A33, MATRIX13:def 1

.= 1_ K by A33, MATRIX_1:def 3 ;

A41: len (Line (A,I)) = m by A12, MATRIX_0:def 7;

A42: I = (idseq n) . I by A27, FINSEQ_2:49

.= (Sgm (Seg n)) . I by FINSEQ_3:48 ;

len (Line (V,jj)) = m by A39, MATRIX_0:def 7;

then len (mlt ((Line (A,I)),(Line (V,jj)))) = m by A41, MATRIX_3:6;

then A43: dom (mlt ((Line (A,I)),(Line (V,jj)))) = Seg m by FINSEQ_1:def 3;

then A44: (mlt ((Line (A,I)),(Line (V,jj)))) /. ((Sgm ((Seg m) \ N)) . jj) = (mlt ((Line (A,I)),(Line (V,jj)))) . ((Sgm ((Seg m) \ N)) . jj) by A8, A36, PARTFUN1:def 6

.= (A * (I,((Sgm ((Seg m) \ N)) . jj))) * (1_ K) by A12, A8, A39, A36, A37, A40, FVSUM_1:61

.= A * (I,((Sgm ((Seg m) \ N)) . jj)) ;

A45: ( Indices V = Indices (0. (K,(m -' n),m)) & rng (Sgm (Seg (m -' n))) = Seg (m -' n) ) by FINSEQ_1:def 13, MATRIX_0:26;

A46: rng (Sgm N) = N by A2, FINSEQ_1:def 13;

A47: rng (Sgm (Seg n)) = Seg n by FINSEQ_1:def 13;

then A60: (Sgm N) . I in N by A27, A46, FUNCT_1:def 3;

then A61: (Sgm ((Seg m) \ N)) . jj <> (Sgm N) . I by A15, A36, XBOOLE_0:3;

[((Sgm (Seg n)) . I),((Sgm N) . I)] in Indices A by A2, A22, A27, A60, A42, ZFMISC_1:87;

then A62: [I,I] in Indices (Segm (A,(Seg n),N)) by A23, A46, A47, MATRIX13:17;

Indices V = [:(Seg (m -' n)),(Seg m):] by A38, MATRIX_0:23;

then [((Sgm (Seg (m -' n))) . jj),((Sgm N) . I)] in Indices V by A2, A29, A60, A31, ZFMISC_1:87;

then A63: [jj,I] in Indices (Segm (V,(Seg (m -' n)),N)) by A9, A46, A45, MATRIX13:17;

A64: Indices SAT = Indices ((Segm (A,(Seg n),((Seg m) \ N))) @) by Lm1;

then A65: [I,jj] in Indices (Segm (A,(Seg n),((Seg m) \ N))) by A16, A63, MATRIX_0:def 6;

A66: (Line (V,jj)) . ((Sgm N) . I) = V * (jj,((Sgm N) . I)) by A2, A39, A60, MATRIX_0:def 7

.= (Segm (V,(Seg (m -' n)),N)) * (jj,I) by A31, A63, MATRIX13:def 1

.= - (((Segm (A,(Seg n),((Seg m) \ N))) @) * (jj,I)) by A16, A63, A64, MATRIX_3:def 2

.= - ((Segm (A,(Seg n),((Seg m) \ N))) * (I,jj)) by A65, MATRIX_0:def 6

.= - (A * (I,((Sgm ((Seg m) \ N)) . jj))) by A42, A65, MATRIX13:def 1 ;

A67: (Line (A,I)) . ((Sgm N) . I) = A * (I,((Sgm N) . I)) by A2, A12, A60, MATRIX_0:def 7

.= (Segm (A,(Seg n),N)) * (I,I) by A42, A62, MATRIX13:def 1

.= 1_ K by A3, A62, MATRIX_1:def 3 ;

(mlt ((Line (A,I)),(Line (V,jj)))) /. ((Sgm N) . I) = (mlt ((Line (A,I)),(Line (V,jj)))) . ((Sgm N) . I) by A2, A43, A60, PARTFUN1:def 6

.= (1_ K) * (- (A * (I,((Sgm ((Seg m) \ N)) . jj)))) by A2, A12, A39, A60, A67, A66, FVSUM_1:61

.= - (A * (I,((Sgm ((Seg m) \ N)) . jj))) ;

then Sum (mlt ((Line (A,I)),(Line (V,jj)))) = (A * (I,((Sgm ((Seg m) \ N)) . jj))) + (- (A * (I,((Sgm ((Seg m) \ N)) . jj)))) by A2, A8, A43, A60, A36, A44, A61, A48, Th7

.= 0. K by VECTSP_1:16 ;

hence (0. (K,n,l)) * (i,j) = (Line (A,I)) "*" (Line (V,jj)) by A25, A24, MATRIX_3:1

.= AM * (i,j) by A12, A19, A25, A30, MATRIX_3:def 4 ;

:: thesis: verum

end;A29: jj in Seg (m -' n) and

A30: Col (M,J) = Line (V,jj) ;

A31: jj = (idseq (m -' n)) . jj by A29, FINSEQ_2:49

.= (Sgm (Seg (m -' n))) . jj by FINSEQ_3:48 ;

A32: Indices (1. (K,(m -' n))) = [:(Seg (m -' n)),(Seg (m -' n)):] by MATRIX_0:24;

then A33: [jj,jj] in Indices (1. (K,(m -' n))) by A29, ZFMISC_1:87;

A34: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by A8, FINSEQ_1:def 13;

A35: dom (Sgm ((Seg m) \ N)) = Seg (m -' n) by A14, A7, FINSEQ_3:40, XBOOLE_1:36;

then A36: (Sgm ((Seg m) \ N)) . jj in (Seg m) \ N by A29, A34, FUNCT_1:def 3;

then A37: (Line (A,I)) . ((Sgm ((Seg m) \ N)) . jj) = A * (I,((Sgm ((Seg m) \ N)) . jj)) by A12, A8, MATRIX_0:def 7;

A38: m -' n <> 0 by A29;

then A39: width V = m by MATRIX_0:23;

then A40: (Line (V,jj)) . ((Sgm ((Seg m) \ N)) . jj) = V * (jj,((Sgm ((Seg m) \ N)) . jj)) by A8, A36, MATRIX_0:def 7

.= (1. (K,(m -' n))) * (jj,jj) by A17, A31, A33, MATRIX13:def 1

.= 1_ K by A33, MATRIX_1:def 3 ;

A41: len (Line (A,I)) = m by A12, MATRIX_0:def 7;

A42: I = (idseq n) . I by A27, FINSEQ_2:49

.= (Sgm (Seg n)) . I by FINSEQ_3:48 ;

len (Line (V,jj)) = m by A39, MATRIX_0:def 7;

then len (mlt ((Line (A,I)),(Line (V,jj)))) = m by A41, MATRIX_3:6;

then A43: dom (mlt ((Line (A,I)),(Line (V,jj)))) = Seg m by FINSEQ_1:def 3;

then A44: (mlt ((Line (A,I)),(Line (V,jj)))) /. ((Sgm ((Seg m) \ N)) . jj) = (mlt ((Line (A,I)),(Line (V,jj)))) . ((Sgm ((Seg m) \ N)) . jj) by A8, A36, PARTFUN1:def 6

.= (A * (I,((Sgm ((Seg m) \ N)) . jj))) * (1_ K) by A12, A8, A39, A36, A37, A40, FVSUM_1:61

.= A * (I,((Sgm ((Seg m) \ N)) . jj)) ;

A45: ( Indices V = Indices (0. (K,(m -' n),m)) & rng (Sgm (Seg (m -' n))) = Seg (m -' n) ) by FINSEQ_1:def 13, MATRIX_0:26;

A46: rng (Sgm N) = N by A2, FINSEQ_1:def 13;

A47: rng (Sgm (Seg n)) = Seg n by FINSEQ_1:def 13;

A48: now :: thesis: for kk being Nat st kk in Seg m & kk <> (Sgm ((Seg m) \ N)) . jj & kk <> (Sgm N) . I holds

(mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

dom (Sgm N) = Seg n
by A1, A2, FINSEQ_3:40;(mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

let kk be Nat; :: thesis: ( kk in Seg m & kk <> (Sgm ((Seg m) \ N)) . jj & kk <> (Sgm N) . I implies (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K )

assume that

A49: kk in Seg m and

A50: kk <> (Sgm ((Seg m) \ N)) . jj and

A51: kk <> (Sgm N) . I ; :: thesis: (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

end;assume that

A49: kk in Seg m and

A50: kk <> (Sgm ((Seg m) \ N)) . jj and

A51: kk <> (Sgm N) . I ; :: thesis: (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

now :: thesis: (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. Kend;

hence
(mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K
; :: thesis: verumper cases
( kk in N or kk in (Seg m) \ N )
by A49, XBOOLE_0:def 5;

end;

suppose
kk in N
; :: thesis: (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

then consider x being object such that

A52: x in dom (Sgm N) and

A53: (Sgm N) . x = kk by A46, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A52;

A54: (Line (V,jj)) . ((Sgm N) . x) = V * (jj,((Sgm N) . x)) by A39, A49, A53, MATRIX_0:def 7;

[((Sgm (Seg n)) . I),((Sgm N) . x)] in Indices A by A22, A27, A42, A49, A53, ZFMISC_1:87;

then A55: [I,x] in Indices (Segm (A,(Seg n),N)) by A23, A46, A47, MATRIX13:17;

(Line (A,I)) . ((Sgm N) . x) = A * (I,((Sgm N) . x)) by A12, A49, A53, MATRIX_0:def 7

.= (Segm (A,(Seg n),N)) * (I,x) by A42, A55, MATRIX13:def 1

.= 0. K by A3, A51, A53, A55, MATRIX_1:def 3 ;

hence (mlt ((Line (A,I)),(Line (V,jj)))) . kk = (0. K) * (V * (jj,((Sgm N) . x))) by A12, A39, A49, A53, A54, FVSUM_1:61

.= 0. K ;

:: thesis: verum

end;A52: x in dom (Sgm N) and

A53: (Sgm N) . x = kk by A46, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A52;

A54: (Line (V,jj)) . ((Sgm N) . x) = V * (jj,((Sgm N) . x)) by A39, A49, A53, MATRIX_0:def 7;

[((Sgm (Seg n)) . I),((Sgm N) . x)] in Indices A by A22, A27, A42, A49, A53, ZFMISC_1:87;

then A55: [I,x] in Indices (Segm (A,(Seg n),N)) by A23, A46, A47, MATRIX13:17;

(Line (A,I)) . ((Sgm N) . x) = A * (I,((Sgm N) . x)) by A12, A49, A53, MATRIX_0:def 7

.= (Segm (A,(Seg n),N)) * (I,x) by A42, A55, MATRIX13:def 1

.= 0. K by A3, A51, A53, A55, MATRIX_1:def 3 ;

hence (mlt ((Line (A,I)),(Line (V,jj)))) . kk = (0. K) * (V * (jj,((Sgm N) . x))) by A12, A39, A49, A53, A54, FVSUM_1:61

.= 0. K ;

:: thesis: verum

suppose
kk in (Seg m) \ N
; :: thesis: (mlt ((Line (A,I)),(Line (V,jj)))) . kk = 0. K

then consider x being object such that

A56: x in dom (Sgm ((Seg m) \ N)) and

A57: (Sgm ((Seg m) \ N)) . x = kk by A34, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A56;

A58: (Line (A,I)) . ((Sgm ((Seg m) \ N)) . x) = A * (I,((Sgm ((Seg m) \ N)) . x)) by A12, A49, A57, MATRIX_0:def 7;

A59: [jj,x] in Indices (1. (K,(m -' n))) by A29, A35, A32, A56, ZFMISC_1:87;

(Line (V,jj)) . ((Sgm ((Seg m) \ N)) . x) = V * (jj,((Sgm ((Seg m) \ N)) . x)) by A39, A49, A57, MATRIX_0:def 7

.= (1. (K,(m -' n))) * (jj,x) by A17, A31, A59, MATRIX13:def 1

.= 0. K by A50, A57, A59, MATRIX_1:def 3 ;

hence (mlt ((Line (A,I)),(Line (V,jj)))) . kk = (A * (I,((Sgm ((Seg m) \ N)) . x))) * (0. K) by A12, A39, A49, A57, A58, FVSUM_1:61

.= 0. K ;

:: thesis: verum

end;A56: x in dom (Sgm ((Seg m) \ N)) and

A57: (Sgm ((Seg m) \ N)) . x = kk by A34, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A56;

A58: (Line (A,I)) . ((Sgm ((Seg m) \ N)) . x) = A * (I,((Sgm ((Seg m) \ N)) . x)) by A12, A49, A57, MATRIX_0:def 7;

A59: [jj,x] in Indices (1. (K,(m -' n))) by A29, A35, A32, A56, ZFMISC_1:87;

(Line (V,jj)) . ((Sgm ((Seg m) \ N)) . x) = V * (jj,((Sgm ((Seg m) \ N)) . x)) by A39, A49, A57, MATRIX_0:def 7

.= (1. (K,(m -' n))) * (jj,x) by A17, A31, A59, MATRIX13:def 1

.= 0. K by A50, A57, A59, MATRIX_1:def 3 ;

hence (mlt ((Line (A,I)),(Line (V,jj)))) . kk = (A * (I,((Sgm ((Seg m) \ N)) . x))) * (0. K) by A12, A39, A49, A57, A58, FVSUM_1:61

.= 0. K ;

:: thesis: verum

then A60: (Sgm N) . I in N by A27, A46, FUNCT_1:def 3;

then A61: (Sgm ((Seg m) \ N)) . jj <> (Sgm N) . I by A15, A36, XBOOLE_0:3;

[((Sgm (Seg n)) . I),((Sgm N) . I)] in Indices A by A2, A22, A27, A60, A42, ZFMISC_1:87;

then A62: [I,I] in Indices (Segm (A,(Seg n),N)) by A23, A46, A47, MATRIX13:17;

Indices V = [:(Seg (m -' n)),(Seg m):] by A38, MATRIX_0:23;

then [((Sgm (Seg (m -' n))) . jj),((Sgm N) . I)] in Indices V by A2, A29, A60, A31, ZFMISC_1:87;

then A63: [jj,I] in Indices (Segm (V,(Seg (m -' n)),N)) by A9, A46, A45, MATRIX13:17;

A64: Indices SAT = Indices ((Segm (A,(Seg n),((Seg m) \ N))) @) by Lm1;

then A65: [I,jj] in Indices (Segm (A,(Seg n),((Seg m) \ N))) by A16, A63, MATRIX_0:def 6;

A66: (Line (V,jj)) . ((Sgm N) . I) = V * (jj,((Sgm N) . I)) by A2, A39, A60, MATRIX_0:def 7

.= (Segm (V,(Seg (m -' n)),N)) * (jj,I) by A31, A63, MATRIX13:def 1

.= - (((Segm (A,(Seg n),((Seg m) \ N))) @) * (jj,I)) by A16, A63, A64, MATRIX_3:def 2

.= - ((Segm (A,(Seg n),((Seg m) \ N))) * (I,jj)) by A65, MATRIX_0:def 6

.= - (A * (I,((Sgm ((Seg m) \ N)) . jj))) by A42, A65, MATRIX13:def 1 ;

A67: (Line (A,I)) . ((Sgm N) . I) = A * (I,((Sgm N) . I)) by A2, A12, A60, MATRIX_0:def 7

.= (Segm (A,(Seg n),N)) * (I,I) by A42, A62, MATRIX13:def 1

.= 1_ K by A3, A62, MATRIX_1:def 3 ;

(mlt ((Line (A,I)),(Line (V,jj)))) /. ((Sgm N) . I) = (mlt ((Line (A,I)),(Line (V,jj)))) . ((Sgm N) . I) by A2, A43, A60, PARTFUN1:def 6

.= (1_ K) * (- (A * (I,((Sgm ((Seg m) \ N)) . jj)))) by A2, A12, A39, A60, A67, A66, FVSUM_1:61

.= - (A * (I,((Sgm ((Seg m) \ N)) . jj))) ;

then Sum (mlt ((Line (A,I)),(Line (V,jj)))) = (A * (I,((Sgm ((Seg m) \ N)) . jj))) + (- (A * (I,((Sgm ((Seg m) \ N)) . jj)))) by A2, A8, A43, A60, A36, A44, A61, A48, Th7

.= 0. K by VECTSP_1:16 ;

hence (0. (K,n,l)) * (i,j) = (Line (A,I)) "*" (Line (V,jj)) by A25, A24, MATRIX_3:1

.= AM * (i,j) by A12, A19, A25, A30, MATRIX_3:def 4 ;

:: thesis: verum

suppose
Col (M,J) = m |-> (0. K)
; :: thesis: AM * (i,j) = (0. (K,n,l)) * (i,j)

hence AM * (i,j) =
(Line (A,I)) "*" (m |-> (0. K))
by A12, A19, A25, MATRIX_3:def 4

.= Sum ((0. K) * (Line (A,I))) by A12, FVSUM_1:66

.= (0. K) * (Sum (Line (A,I))) by FVSUM_1:73

.= 0. K

.= (0. (K,n,l)) * (i,j) by A25, A24, MATRIX_3:1 ;

:: thesis: verum

end;.= Sum ((0. K) * (Line (A,I))) by A12, FVSUM_1:66

.= (0. K) * (Sum (Line (A,I))) by FVSUM_1:73

.= 0. K

.= (0. (K,n,l)) * (i,j) by A25, A24, MATRIX_3:1 ;

:: thesis: verum

hence M in Solutions_of (A,(0. (K,n,l))) by A12, A19, A20, A21; :: thesis: verum