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 S₁[ 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 S₁[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 S₁[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 S₁[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 S₁[i,j,x]

per cases ( j = 1 or j <> 1 ) ;

suppose j = 1 ; :: thesis: ex x being Element of K st S₁[i,j,x]

hence ex x being Element of K st S₁[i,j,x] by A6; :: thesis: verum

end;

suppose j <> 1 ; :: thesis: ex x being Element of K st S₁[i,j,x]

hence ex x being Element of K st S₁[i,j,x] by A6; :: thesis: verum

end;

end;

end;

suppose A7: i <> 1 ; :: thesis: ex x being Element of K st S₁[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 S₁[i,j,x] by A7; :: thesis: verum

end;

end;

end;

consider P0 being Matrix of n,n,K such that
A8: for i, j being Nat st [i,j] in Indices P0 holds
S₁[i,j,P0 * (i,j)] from MATRIX_0:sch 2(A4);
A9: 0 + 1 <= n by A1, NAT_1:13;
A10: 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
A11: 1 < i and
A12: i <= n ; :: thesis: P0 . i = Base_FinSeq (K,n,i)
[i,1] in Indices P0 by A9, A11, A12, MATRIX_0:31;
then consider p being FinSequence of K such that
A13: p = P0 . i and
P0 * (i,1) = p . 1 by MATRIX_0:def 5;
A14: 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 A15: [i,j] in Indices P0 by A11, A12, MATRIX_0:31;
then ex p2 being FinSequence of K st
( p2 = P0 . i & P0 * (i,j) = p2 . j ) by MATRIX_0:def 5;
hence p . j = (Base_FinSeq (K,n,i)) . j by A8, A11, A13, A15; :: thesis: verum

end;

len P0 = n by MATRIX_0:def 2;
then i in Seg (len P0) by A11, A12, FINSEQ_1:1;
then i in dom P0 by FINSEQ_1:def 3;
then p in rng P0 by A13, FUNCT_1:def 3;
then A16: len p = n by MATRIX_0:def 2;
len (Base_FinSeq (K,n,i)) = n by Th23;
hence P0 . i = Base_FinSeq (K,n,i) by A13, A16, A14, FINSEQ_1:14; :: thesis: verum

end;

A17: len (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A18: Indices P0 = [:(Seg n),(Seg n):] by MATRIX_0:24;
A19: len (Base_FinSeq (K,n,1)) = n by Th23;
A20: [1,1] in Indices P0 by A9, MATRIX_0:31;
then A21: P0 * (1,1) = (A * (1,1)) " by A8;
then A22: P0 is invertible by A1, A2, A10, Th38;
A23: len P0 = n by MATRIX_0:24;
then A24: 1 in Seg (len P0) by A9, FINSEQ_1:1;
A25: 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
A26: 1 <= k and
A27: k <= n ; :: thesis: (Col (P0,1)) . k = (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k
A28: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A19, A26, A27, FINSEQ_4:15;
k in Seg n by A26, A27, FINSEQ_1:1;
then A29: k in dom (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) by A17, FINSEQ_1:def 3;

A30: now :: thesis: ( k <> 1 implies (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k = 0. K )

assume A31: 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 A29, A28, FVSUM_1:50
.= ((A * (1,1)) ") * (0. K) by A26, A27, A28, A31, Th25
.= 0. K ; :: thesis: verum

end;

k in Seg n by A26, A27, FINSEQ_1:1;
then A32: k in dom P0 by A23, FINSEQ_1:def 3;

A33: now :: thesis: ( k <> 1 implies (Col (P0,1)) . k = 0. K )

k in Seg n by A26, A27, FINSEQ_1:1;
then [k,1] in Indices P0 by A23, A24, A18, ZFMISC_1:87;
then A34: ex p being FinSequence of K st
( p = P0 . k & P0 * (k,1) = p . 1 ) by MATRIX_0:def 5;
assume A35: k <> 1 ; :: thesis: (Col (P0,1)) . k = 0. K
then ( k in NAT & 1 < k ) by A26, ORDINAL1:def 12, XXREAL_0:1;
then P0 * (k,1) = (Base_FinSeq (K,n,k)) . 1 by A10, A27, A34
.= 0. K by A9, A35, Th25 ;
hence (Col (P0,1)) . k = 0. K by A32, MATRIX_0:def 8; :: thesis: verum

end;

A36: now :: thesis: ( k = 1 implies (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k = (A * (1,1)) " )

assume A37: 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 A29, A28, FVSUM_1:50
.= ((A * (1,1)) ") * (1. K) by A27, A28, A37, Th24
.= (A * (1,1)) " ;
:: thesis: verum

end;

1 <= n by A26, A27, XXREAL_0:2;
then 1 in dom P0 by A23, FINSEQ_3:25;
hence (Col (P0,1)) . k = (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k by A21, A30, A36, A33, MATRIX_0:def 8; :: thesis: verum

end;

A38: len A = n by MATRIX_0:24;
then A39: 1 in Seg (len A) by A3, FINSEQ_1:1;
then A40: 1 in dom A by FINSEQ_1:def 3;
A41: width A = n by MATRIX_0:24;
then A42: len (Line (A,1)) = n by MATRIX_0:def 7;
then A43: 1 in dom (Line (A,1)) by A38, A39, FINSEQ_1:def 3;
A44: 1 in Seg (width A) by A41, A3, FINSEQ_1:1;
A45: 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
A46: ( 1 < i & i <= n ) and
A47: A * (i,1) = 0. K ; :: thesis: (A * P0) * (i,1) = 0. K
A48: 1 <= n by A46, XXREAL_0:2;
reconsider p = Col (P0,1), q = ((A * (1,1)) ") * (Base_FinSeq (K,n,1)) as FinSequence of K ;
A49: len (Col (P0,1)) = len P0 by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
A50: len (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A51: 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
A52: 1 <= k and
A53: k <= n ; :: thesis: p . k = q . k
A54: len (Base_FinSeq (K,n,1)) = n by Th23;
then A55: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A52, A53, FINSEQ_4:15;
k in dom P0 by A23, A52, A53, FINSEQ_3:25;
then A56: p . k = P0 * (k,1) by MATRIX_0:def 8;
k in dom (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) by A50, A52, A53, FINSEQ_3:25;
then A57: (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k = ((A * (1,1)) ") * ((Base_FinSeq (K,n,1)) /. k) by A55, FVSUM_1:50;

per cases ( 1 = k or 1 < k ) by A52, XXREAL_0:1;

suppose A58: 1 = k ; :: thesis: p . k = q . k

then q . k = ((A * (1,1)) ") * (1. K) by A53, A55, A57, Th24
.= (A * (1,1)) " ;
hence p . k = q . k by A8, A20, A56, A58; :: thesis: verum

end;

suppose A59: 1 < k ; :: thesis: p . k = q . k

(Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A52, A53, A54, FINSEQ_4:15;
then A60: ((A * (1,1)) ") * ((Base_FinSeq (K,n,1)) /. k) = ((A * (1,1)) ") * (0. K) by A53, A59, Th25
.= 0. K ;
[k,1] in Indices P0 by A48, A52, A53, MATRIX_0:31;
then A61: ex p2 being FinSequence of K st
( p2 = P0 . k & P0 * (k,1) = p2 . 1 ) by MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then p . k = (Base_FinSeq (K,n,k)) . 1 by A10, A53, A56, A59, A61;
hence p . k = q . k by A48, A57, A59, A60, Th25; :: thesis: verum

end;

end;

end;

A62: width A = n by MATRIX_0:24;
then A63: len (Line (A,i)) = n by MATRIX_0:def 7;
then A64: (Line (A,i)) /. 1 = (Line (A,i)) . 1 by A3, FINSEQ_4:15
.= A * (i,1) by A44, MATRIX_0:def 7 ;
[i,1] in Indices (A * P0) by A46, A48, MATRIX_0:31;
hence (A * P0) * (i,1) = |((Line (A,i)),(Col (P0,1)))| by A23, A62, MATRIX_3:def 4
.= |((Line (A,i)),(((A * (1,1)) ") * (Base_FinSeq (K,n,1))))| by A49, A50, A51, FINSEQ_1:14
.= ((A * (1,1)) ") * |((Line (A,i)),(Base_FinSeq (K,n,1)))| by A19, A63, Th10
.= ((A * (1,1)) ") * (A * (i,1)) by A3, A63, A64, Th35
.= 0. K by A47 ;
:: thesis: verum

end;

A65: 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
A66: 1 < j and
A67: j <= n ; :: thesis: (A * P0) * (1,j) = 0. K
A68: 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 ;
A69: len ((- (((A * (1,1)) ") * (A * (1,j)))) * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A70: 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 ;
A71: [1,j] in Indices P0 by A9, A66, A67, MATRIX_0:31;
A72: for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

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 ;
let k be Nat; :: thesis: ( 1 <= k & k <= n implies p . k = q . k )
assume that
A74: 1 <= k and
A75: k <= n ; :: thesis: p . k = q . k
k in Seg n by A74, A75, FINSEQ_1:1;
then A76: k in dom ((- (((A * (1,1)) ") * (A * (1,j)))) * (Base_FinSeq (K,n,1))) by A69, FINSEQ_1:def 3;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A77: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A74, A75, FINSEQ_4:15;
A78: (- ((((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 A76, A77, FVSUM_1:50 ;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A79: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A74, A75, FINSEQ_4:15;
k in dom P0 by A23, A74, A75, FINSEQ_3:25;
then A80: p . k = P0 * (k,j) by MATRIX_0:def 8;

per cases ( 1 = k or 1 < k ) by A74, XXREAL_0:1;

suppose A81: 1 = k ; :: thesis: p . k = q . k

k <= len (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) by A75, A73, Th6;
then 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 A74, A78, FINSEQ_4:15
.= (- (((A * (1,1)) ") * (A * (1,j)))) * (1. K) by A75, A79, A81, Th24
.= - (((A * (1,1)) ") * (A * (1,j))) ;
A83: p . k = - (((A * (1,1)) ") * (A * (1,j))) by A8, A66, A71, A80, A81;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A68, A74, A75, FINSEQ_4:15
.= 0. K by A66, A75, A81, Th25 ;
then q . k = (- (((A * (1,1)) ") * (A * (1,j)))) + (0. K) by A70, A68, A74, A75, A82, Th5;
hence p . k = q . k by A83, RLVECT_1:4; :: thesis: verum

end;

suppose A84: 1 < k ; :: thesis: p . k = q . k

( [k,j] in Indices P0 & k in NAT ) by A66, A67, A74, A75, MATRIX_0:31, ORDINAL1:def 12;
then A85: p . k = (Base_FinSeq (K,n,k)) . j by A8, A80, A84;

per cases ( k <> j or k = j ) ;

suppose A86: 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 A74, A75, FINSEQ_4:15;
then A87: (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- (((A * (1,1)) ") * (A * (1,j)))) * (0. K) by A75, A78, A84, Th25
.= 0. K ;
A88: (- ((((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 A70, A74, A75, FINSEQ_4:15;
A89: p . k = 0. K by A66, A67, A85, A86, Th25;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A68, A74, A75, FINSEQ_4:15
.= 0. K by A74, A75, A86, Th25 ;
then q . k = (0. K) + (0. K) by A70, A68, A74, A75, A88, A87, Th5;
hence p . k = q . k by A89, RLVECT_1:4; :: thesis: verum

end;

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 A74, A75, 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 A75, A78, A84, Th25
.= 0. K ;
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 A70, A74, A75, FINSEQ_4:15;
A93: p . k = 1. K by A74, A75, A85, A90, Th24;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A68, A74, A75, FINSEQ_4:15
.= 1. K by A74, A75, A90, Th24 ;
then q . k = (0. K) + (1. K) by A70, A68, A74, A75, A92, A91, Th5;
hence p . k = q . k by A93, RLVECT_1:4; :: thesis: verum

end;

end;

end;

end;

end;

A94: width A = n by MATRIX_0:24;
then A95: len (Line (A,1)) = n by MATRIX_0:def 7;
then A96: (Line (A,1)) /. 1 = (Line (A,1)) . 1 by A3, FINSEQ_4:15
.= A * (1,1) by A44, MATRIX_0:def 7 ;
A97: j in Seg n by A66, A67, FINSEQ_1:1;
A98: len (Col (P0,j)) = len P0 by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
len ((- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j))) = n by A70, A68, Th2;
then A99: Col (P0,j) = (- ((((A * (1,1)) ") * (A * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) by A98, A72, FINSEQ_1:14;
A100: (Line (A,1)) /. j = (Line (A,1)) . j by A66, A67, A95, FINSEQ_4:15
.= A * (1,j) by A97, A94, MATRIX_0:def 7 ;
[1,j] in Indices (A * P0) by A9, A66, A67, MATRIX_0:31;
then (A * P0) * (1,j) = |((Line (A,1)),(Col (P0,j)))| by A23, A94, 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 A42, A70, A68, A99, 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 A42, A19, Th10
.= ((- (((A * (1,1)) ") * (A * (1,j)))) * (A * (1,1))) + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by A42, A3, A96, 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 A42, A66, A67, Th35
.= (- (A * (1,j))) + (A * (1,j)) by A100
.= 0. K by RLVECT_1:5 ;
hence (A * P0) * (1,j) = 0. K ; :: thesis: verum

end;

A101: ( Indices A = [:(Seg n),(Seg n):] & Indices (A * P0) = [:(Seg n),(Seg n):] ) by MATRIX_0:24;
A102: len (Col (P0,1)) = len P0 by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
len (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
then A103: Col (P0,1) = ((A * (1,1)) ") * (Base_FinSeq (K,n,1)) by A102, A25, FINSEQ_1:14;
A104: len (((A * (1,1)) ") * (Line (A,1))) = len (Line (A,1)) by MATRIXR1:16
.= n by A41, MATRIX_0:def 7 ;
[1,1] in Indices A by A3, MATRIX_0:31;
then (A * P0) * (1,1) = |((Line (A,1)),(Col (P0,1)))| by A23, A41, A101, MATRIX_3:def 4
.= ((A * (1,1)) ") * |((Line (A,1)),(Base_FinSeq (K,n,1)))| by A42, A19, A103, Th10
.= ((A * (1,1)) ") * ((Line (A,1)) /. 1) by A42, A3, Th35
.= (((A * (1,1)) ") * (Line (A,1))) /. 1 by A43, POLYNOM1:def 1
.= (((A * (1,1)) ") * (Line (A,1))) . 1 by A3, A104, FINSEQ_4:15
.= ((A * (1,1)) ") * (A * (1,1)) by A44, A40, 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 A22, A65, A45; :: thesis: verum