let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds
ex P being Matrix of n,K st
( P is invertible & (A * P) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * (1,j) = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds
(A * P) * (i,1) = 0. K ) )
let K be Field; :: thesis: for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds
ex P being Matrix of n,K st
( P is invertible & (A * P) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * (1,j) = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds
(A * P) * (i,1) = 0. K ) )
let A be Matrix of n,K; :: thesis: ( n > 0 & A * (1,1) <> 0. K implies ex P being Matrix of n,K st
( P is invertible & (A * P) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * (1,j) = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds
(A * P) * (i,1) = 0. K ) ) )
assume that
A1: n > 0 and
A2: A * (1,1) <> 0. K ; :: thesis: ex P being Matrix of n,K st
( P is invertible & (A * P) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * (1,j) = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds
(A * P) * (i,1) = 0. K ) )
A3: 0 + 1 <= n by A1, NAT_1:13;
set a = A * (1,1);
defpred S1[ Nat, Nat, Element of K] means ( ( $1 = 1 implies ( ( $2 = 1 implies $3 = (A * (1,1)) " ) & ( $2 <> 1 implies $3 = - (((A * (1,1)) ") * (A * (1,$2))) ) ) ) & ( $1 <> 1 implies for i0 being Element of NAT st i0 = $1 holds
$3 = (Base_FinSeq (K,n,i0)) . $2 ) );
A4: for i, j being Nat st [i,j] in [:(Seg n),(Seg n):] holds
ex x being Element of K st S1[i,j,x]
proof
let i, j be Nat; :: thesis: ( [i,j] in [:(Seg n),(Seg n):] implies ex x being Element of K st S1[i,j,x] )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;
assume [i,j] in [:(Seg n),(Seg n):] ; :: thesis: ex x being Element of K st S1[i,j,x]
then j0 in Seg n by ZFMISC_1:87;
then A5: ( 1 <= j0 & j0 <= n ) by FINSEQ_1:1;
per cases ( i = 1 or i <> 1 ) ;
suppose A6: i = 1 ; :: thesis: ex x being Element of K st S1[i,j,x]
per cases ( j = 1 or j <> 1 ) ;
suppose j = 1 ; :: thesis: ex x being Element of K st S1[i,j,x]
hence ex x being Element of K st S1[i,j,x] by A6; :: thesis: verum
end;
suppose j <> 1 ; :: thesis: ex x being Element of K st S1[i,j,x]
hence ex x being Element of K st S1[i,j,x] by A6; :: thesis: verum
end;
end;
end;
suppose A7: i <> 1 ; :: thesis: ex x being Element of K st S1[i,j,x]
set x1 = (Base_FinSeq (K,n,i0)) /. j0;
len (Base_FinSeq (K,n,i0)) = n by Th23;
then for i1 being Element of NAT st i1 = i holds
(Base_FinSeq (K,n,i0)) /. j0 = (Base_FinSeq (K,n,i1)) . j by A5, FINSEQ_4:15;
hence ex x being Element of K st S1[i,j,x] by A7; :: thesis: verum
end;
end;
end;
consider P0 being Matrix of n,n,K such that
A12: for i, j being Nat st [i,j] in Indices P0 holds
S1[i,j,P0 * (i,j)] from MATRIX_1:sch 2(A4);
 A13: 0 + 1 <= n by A1, NAT_1:13;
A14: for i being Element of NAT st 1 < i & i <= n holds
P0 . i = Base_FinSeq (K,n,i)
proof
let i be Element of NAT ; :: thesis: ( 1 < i & i <= n implies P0 . i = Base_FinSeq (K,n,i) )
assume that
A15: 1 < i and
A16: i <= n ; :: thesis: P0 . i = Base_FinSeq (K,n,i)
[i,1] in Indices P0 by A13, A15, A16, MATRIX_1:37;
then consider p being FinSequence of K such that
A17: p = P0 . i and
P0 * (i,1) = p . 1 by MATRIX_1:def 5;
A18: for j being Nat st 1 <= j & j <= n holds
p . j = (Base_FinSeq (K,n,i)) . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= n implies p . j = (Base_FinSeq (K,n,i)) . j )
assume ( 1 <= j & j <= n ) ; :: thesis: p . j = (Base_FinSeq (K,n,i)) . j
then A19: [i,j] in Indices P0 by A15, A16, MATRIX_1:37;
then ex p2 being FinSequence of K st
( p2 = P0 . i & P0 * (i,j) = p2 . j ) by MATRIX_1:def 5;
hence p . j = (Base_FinSeq (K,n,i)) . j by A12, A15, A17, A19; :: thesis: verum
end;
len P0 = n by MATRIX_1:def 2;
then i in Seg (len P0) by A15, A16, FINSEQ_1:1;
then i in dom P0 by FINSEQ_1:def 3;
then p in rng P0 by A17, FUNCT_1:def 3;
then A20: len p = n by MATRIX_1:def 2;
len (Base_FinSeq (K,n,i)) = n by Th23;
hence P0 . i = Base_FinSeq (K,n,i) by A17, A20, A18, FINSEQ_1:14; :: thesis: verum
end;
A21: len (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A22: Indices P0 = [:(Seg n),(Seg n):] by MATRIX_1:24;
A23: len (Base_FinSeq (K,n,1)) = n by Th23;
A24: [1,1] in Indices P0 by A13, MATRIX_1:37;
then A25: P0 * (1,1) = (A * (1,1)) " by A12;
then A26: P0 is invertible by A1, A2, A14, Th38;
A27: len P0 = n by MATRIX_1:24;
then A28: 1 in Seg (len P0) by A13, FINSEQ_1:1;
A29: for k being Nat st 1 <= k & k <= n holds
(Col (P0,1)) . k = (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= n implies (Col (P0,1)) . k = (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k )
assume that
A30: 1 <= k and
A31: k <= n ; :: thesis: (Col (P0,1)) . k = (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k
A32: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A23, A30, A31, FINSEQ_4:15;
k in Seg n by A30, A31, FINSEQ_1:1;
then A33: k in dom (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) by A21, FINSEQ_1:def 3;
A34: now
assume A35: k <> 1 ; :: thesis: (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k = 0. K
thus (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k = ((A * (1,1)) ") * ((Base_FinSeq (K,n,1)) /. k) by A33, A32, FVSUM_1:50
.= ((A * (1,1)) ") * (0. K) by A30, A31, A32, A35, Th25
.= 0. K by VECTSP_1:6 ; :: thesis: verum
end;
k in Seg n by A30, A31, FINSEQ_1:1;
then A36: k in dom P0 by A27, FINSEQ_1:def 3;
A37: now
k in Seg n by A30, A31, FINSEQ_1:1;
then [k,1] in Indices P0 by A27, A28, A22, ZFMISC_1:87;
then A38: ex p being FinSequence of K st
( p = P0 . k & P0 * (k,1) = p . 1 ) by MATRIX_1:def 5;
assume A39: k <> 1 ; :: thesis: (Col (P0,1)) . k = 0. K
then ( k in NAT & 1 < k ) by A30, ORDINAL1:def 12, XXREAL_0:1;
then P0 * (k,1) = (Base_FinSeq (K,n,k)) . 1 by A14, A31, A38
.= 0. K by A13, A39, Th25 ;
hence (Col (P0,1)) . k = 0. K by A36, MATRIX_1:def 8; :: thesis: verum
end;
A40: now
assume A41: k = 1 ; :: thesis: (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k = (A * (1,1)) "
hence (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k = ((A * (1,1)) ") * ((Base_FinSeq (K,n,1)) /. 1) by A33, A32, FVSUM_1:50
.= ((A * (1,1)) ") * (1. K) by A31, A32, A41, Th24
.= (A * (1,1)) " by VECTSP_1:def 6 ;
:: thesis: verum
end;
1 <= n by A30, A31, XXREAL_0:2;
then 1 in dom P0 by A27, FINSEQ_3:25;
hence (Col (P0,1)) . k = (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k by A25, A34, A40, A37, MATRIX_1:def 8; :: thesis: verum
end;
A42: len A = n by MATRIX_1:24;
then A43: 1 in Seg (len A) by A3, FINSEQ_1:1;
then A44: 1 in dom A by FINSEQ_1:def 3;
A45: width A = n by MATRIX_1:24;
then A46: len (Line (A,1)) = n by MATRIX_1:def 7;
then A47: 1 in dom (Line (A,1)) by A42, A43, FINSEQ_1:def 3;
A48: 1 in Seg (width A) by A45, A3, FINSEQ_1:1;
A49: for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds
(A * P0) * (i,1) = 0. K
proof
set Q = A;
set P = P0;
let i be Element of NAT ; :: thesis: ( 1 < i & i <= n & A * (i,1) = 0. K implies (A * P0) * (i,1) = 0. K )
assume that
A50: ( 1 < i & i <= n ) and
A51: A * (i,1) = 0. K ; :: thesis: (A * P0) * (i,1) = 0. K
A52: 1 <= n by A50, XXREAL_0:2;
reconsider p = Col (P0,1), q = ((A * (1,1)) ") * (Base_FinSeq (K,n,1)) as FinSequence of K ;
A53: len (Col (P0,1)) = len P0 by MATRIX_1:def 8
.= n by MATRIX_1:24 ;
A54: len (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A55: for k being Nat st 1 <= k & k <= n holds
p . k = q . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume that
A56: 1 <= k and
A57: k <= n ; :: thesis: p . k = q . k
A58: len (Base_FinSeq (K,n,1)) = n by Th23;
then A59: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A56, A57, FINSEQ_4:15;
k in dom P0 by A27, A56, A57, FINSEQ_3:25;
then A60: p . k = P0 * (k,1) by MATRIX_1:def 8;
k in dom (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) by A54, A56, A57, FINSEQ_3:25;
then A61: (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k = ((A * (1,1)) ") * ((Base_FinSeq (K,n,1)) /. k) by A59, FVSUM_1:50;
per cases ( 1 = k or 1 < k ) by A56, XXREAL_0:1;
suppose A62: 1 = k ; :: thesis: p . k = q . k
then q . k = ((A * (1,1)) ") * (1. K) by A57, A59, A61, Th24
.= (A * (1,1)) " by VECTSP_1:def 6 ;
hence p . k = q . k by A12, A24, A60, A62; :: thesis: verum
end;
suppose A63: 1 < k ; :: thesis: p . k = q . k
(Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A56, A57, A58, FINSEQ_4:15;
then A64: ((A * (1,1)) ") * ((Base_FinSeq (K,n,1)) /. k) = ((A * (1,1)) ") * (0. K) by A57, A63, Th25
.= 0. K by VECTSP_1:6 ;
[k,1] in Indices P0 by A52, A56, A57, MATRIX_1:37;
then A65: ex p2 being FinSequence of K st
( p2 = P0 . k & P0 * (k,1) = p2 . 1 ) by MATRIX_1:def 5;
k in NAT by ORDINAL1:def 12;
then p . k = (Base_FinSeq (K,n,k)) . 1 by A14, A57, A60, A63, A65;
hence p . k = q . k by A52, A61, A63, A64, Th25; :: thesis: verum
end;
end;
end;
A66: width A = n by MATRIX_1:24;
then A67: len (Line (A,i)) = n by MATRIX_1:def 7;
then A68: (Line (A,i)) /. 1 = (Line (A,i)) . 1 by A3, FINSEQ_4:15
.= A * (i,1) by A48, MATRIX_1:def 7 ;
[i,1] in Indices (A * P0) by A50, A52, MATRIX_1:37;
hence (A * P0) * (i,1) = |((Line (A,i)),(Col (P0,1)))| by A27, A66, MATRIX_3:def 4
.= |((Line (A,i)),(((A * (1,1)) ") * (Base_FinSeq (K,n,1))))| by A53, A54, A55, FINSEQ_1:14
.= ((A * (1,1)) ") * |((Line (A,i)),(Base_FinSeq (K,n,1)))| by A23, A67, Th10
.= ((A * (1,1)) ") * (A * (i,1)) by A3, A67, A68, Th35
.= 0. K by A51, VECTSP_1:6 ;
:: thesis: verum
end;
A69: for j being Element of NAT st 1 < j & j <= n holds
(A * P0) * (1,j) = 0. K
proof
let j be Element of NAT ; :: thesis: ( 1 < j & j <= n implies (A * P0) * (1,j) = 0. K )
assume that
A70: 1 < j and
A71: j <= n ; :: thesis: (A * P0) * (1,j) = 0. K
A72: len (Base_FinSeq (K,n,j)) = n by Th23;
reconsider p = Col (P0,j), q = (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) as FinSequence of K ;
A73: len ((- (((A * (1,1)) ") * (A * (1,j)))) * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A74: len (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) = len ((- (((A * (1,1)) ") * (A * (1,j)))) * (Base_FinSeq (K,n,1))) by Th6
.= len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A75: [1,j] in Indices P0 by A13, A70, A71, MATRIX_1:37;
A76: for k being Nat st 1 <= k & k <= n holds
p . k = q . k
proof
A77: len ((- (((A * (1,1)) ") * (A * (1,j)))) * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume that
A78: 1 <= k and
A79: k <= n ; :: thesis: p . k = q . k
k in Seg n by A78, A79, FINSEQ_1:1;
then A80: k in dom ((- (((A * (1,1)) ") * (A * (1,j)))) * (Base_FinSeq (K,n,1))) by A73, FINSEQ_1:def 3;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A81: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A78, A79, FINSEQ_4:15;
A82: (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) . k = ((- (((A * (1,1)) ") * (A * (1,j)))) * (Base_FinSeq (K,n,1))) . k by Th6
.= (- (((A * (1,1)) ") * (A * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A80, A81, FVSUM_1:50 ;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A83: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A78, A79, FINSEQ_4:15;
k in dom P0 by A27, A78, A79, FINSEQ_3:25;
then A84: p . k = P0 * (k,j) by MATRIX_1:def 8;
per cases ( 1 = k or 1 < k ) by A78, XXREAL_0:1;
suppose A85: 1 = k ; :: thesis: p . k = q . k
k <= len (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) by A79, A77, Th6;
then A86: (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- (((A * (1,1)) ") * (A * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A78, A82, FINSEQ_4:15
.= (- (((A * (1,1)) ") * (A * (1,j)))) * (1. K) by A79, A83, A85, Th24
.= - (((A * (1,1)) ") * (A * (1,j))) by VECTSP_1:def 6 ;
A87: p . k = - (((A * (1,1)) ") * (A * (1,j))) by A12, A70, A75, A84, A85;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A72, A78, A79, FINSEQ_4:15
.= 0. K by A70, A79, A85, Th25 ;
then q . k = (- (((A * (1,1)) ") * (A * (1,j)))) + (0. K) by A74, A72, A78, A79, A86, Th5;
hence p . k = q . k by A87, RLVECT_1:4; :: thesis: verum
end;
suppose A88: 1 < k ; :: thesis: p . k = q . k
( [k,j] in Indices P0 & k in NAT ) by A70, A71, A78, A79, MATRIX_1:37, ORDINAL1:def 12;
then A89: p . k = (Base_FinSeq (K,n,k)) . j by A12, A84, A88;
per cases ( k <> j or k = j ) ;
suppose A90: k <> j ; :: thesis: p . k = q . k
len (Base_FinSeq (K,n,1)) = n by Th23;
then (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A78, A79, FINSEQ_4:15;
then A91: (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- (((A * (1,1)) ") * (A * (1,j)))) * (0. K) by A79, A82, A88, Th25
.= 0. K by VECTSP_1:6 ;
A92: (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A74, A78, A79, FINSEQ_4:15;
A93: p . k = 0. K by A70, A71, A89, A90, Th25;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A72, A78, A79, FINSEQ_4:15
.= 0. K by A78, A79, A90, Th25 ;
then q . k = (0. K) + (0. K) by A74, A72, A78, A79, A92, A91, Th5;
hence p . k = q . k by A93, RLVECT_1:4; :: thesis: verum
end;
suppose A94: k = j ; :: thesis: p . k = q . k
len (Base_FinSeq (K,n,1)) = n by Th23;
then (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A78, A79, FINSEQ_4:15;
then A95: (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- (((A * (1,1)) ") * (A * (1,j)))) * (0. K) by A79, A82, A88, Th25
.= 0. K by VECTSP_1:6 ;
A96: (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A74, A78, A79, FINSEQ_4:15;
A97: p . k = 1. K by A78, A79, A89, A94, Th24;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A72, A78, A79, FINSEQ_4:15
.= 1. K by A78, A79, A94, Th24 ;
then q . k = (0. K) + (1. K) by A74, A72, A78, A79, A96, A95, Th5;
hence p . k = q . k by A97, RLVECT_1:4; :: thesis: verum
end;
end;
end;
end;
end;
A98: width A = n by MATRIX_1:24;
then A99: len (Line (A,1)) = n by MATRIX_1:def 7;
then A100: (Line (A,1)) /. 1 = (Line (A,1)) . 1 by A3, FINSEQ_4:15
.= A * (1,1) by A48, MATRIX_1:def 7 ;
A101: j in Seg n by A70, A71, FINSEQ_1:1;
A102: len (Col (P0,j)) = len P0 by MATRIX_1:def 8
.= n by MATRIX_1:24 ;
len ((- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j))) = n by A74, A72, Th2;
then A103: Col (P0,j) = (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) by A102, A76, FINSEQ_1:14;
A104: (Line (A,1)) /. j = (Line (A,1)) . j by A70, A71, A99, FINSEQ_4:15
.= A * (1,j) by A101, A98, MATRIX_1:def 7 ;
[1,j] in Indices (A * P0) by A13, A70, A71, MATRIX_1:37;
then (A * P0) * (1,j) = |((Line (A,1)),(Col (P0,j)))| by A27, A98, MATRIX_3:def 4
.= |((Line (A,1)),(- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))))| + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by A46, A74, A72, A103, Th11
.= |((Line (A,1)),((- (((A * (1,1)) ") * (A * (1,j)))) * (Base_FinSeq (K,n,1))))| + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by Th6
.= ((- (((A * (1,1)) ") * (A * (1,j)))) * |((Line (A,1)),(Base_FinSeq (K,n,1)))|) + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by A46, A23, Th10
.= ((- (((A * (1,1)) ") * (A * (1,j)))) * (A * (1,1))) + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by A46, A3, A100, Th35
.= (- ((((A * (1,1)) ") * (A * (1,j))) * (A * (1,1)))) + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by VECTSP_1:9
.= (- ((A * (1,j)) * (((A * (1,1)) ") * (A * (1,1))))) + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by GROUP_1:def 3
.= (- ((A * (1,j)) * (1. K))) + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by A2, VECTSP_1:def 10
.= (- ((A * (1,j)) * (1. K))) + ((Line (A,1)) /. j) by A46, A70, A71, Th35
.= (- (A * (1,j))) + (A * (1,j)) by A104, VECTSP_1:def 6
.= 0. K by RLVECT_1:5 ;
hence (A * P0) * (1,j) = 0. K ; :: thesis: verum
end;
A105: ( Indices A = [:(Seg n),(Seg n):] & Indices (A * P0) = [:(Seg n),(Seg n):] ) by MATRIX_1:24;
A106: len (Col (P0,1)) = len P0 by MATRIX_1:def 8
.= n by MATRIX_1:24 ;
len (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
then A107: Col (P0,1) = ((A * (1,1)) ") * (Base_FinSeq (K,n,1)) by A106, A29, FINSEQ_1:14;
A108: len (((A * (1,1)) ") * (Line (A,1))) = len (Line (A,1)) by MATRIXR1:16
.= n by A45, MATRIX_1:def 7 ;
[1,1] in Indices A by A3, MATRIX_1:37;
then (A * P0) * (1,1) = |((Line (A,1)),(Col (P0,1)))| by A27, A45, A105, MATRIX_3:def 4
.= ((A * (1,1)) ") * |((Line (A,1)),(Base_FinSeq (K,n,1)))| by A46, A23, A107, Th10
.= ((A * (1,1)) ") * ((Line (A,1)) /. 1) by A46, A3, Th35
.= (((A * (1,1)) ") * (Line (A,1))) /. 1 by A47, POLYNOM1:def 1
.= (((A * (1,1)) ") * (Line (A,1))) . 1 by A3, A108, FINSEQ_4:15
.= ((A * (1,1)) ") * (A * (1,1)) by A48, A44, MATRIX12:3
.= 1. K by A2, VECTSP_1:def 10 ;
hence ex P being Matrix of n,K st
( P is invertible & (A * P) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * (1,j) = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds
(A * P) * (i,1) = 0. K ) ) by A26, A69, A49; :: thesis: verum