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 13;
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:106;
then A5: ( 1 <= j0 & j0 <= n ) by FINSEQ_1:3;

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

end;

end;

end;

A8: for i, j being Nat st [i,j] in [:(Seg n),(Seg n):] holds
for x1, x2 being Element of K st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg n),(Seg n):] implies for x1, x2 being Element of K st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 )
assume [i,j] in [:(Seg n),(Seg n):] ; :: thesis: for x1, x2 being Element of K st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2
reconsider i0 = i as Element of NAT by ORDINAL1:def 13;
let x1, x2 be Element of K; :: thesis: ( S₁[i,j,x1] & S₁[i,j,x2] implies x1 = x2 )
assume that
A9: S₁[i,j,x1] and
A10: S₁[i,j,x2] ; :: thesis: x1 = x2

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

suppose i = 1 ; :: thesis: x1 = x2

hence x1 = x2 by A9, A10; :: thesis: verum

end;

suppose A11: i <> 1 ; :: thesis: x1 = x2

then x1 = (Base_FinSeq (K,n,i0)) . j by A9;
hence x1 = x2 by A10, A11; :: 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
S₁[i,j,P0 * (i,j)] from MATRIX_1:sch 2(A8, 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:38;
then consider p being FinSequence of K such that
A17: p = P0 . i and
P0 * (i,1) = p . 1 by MATRIX_1:def 6;
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:38;
then ex p2 being FinSequence of K st
( p2 = P0 . i & P0 * (i,j) = p2 . j ) by MATRIX_1:def 6;
hence p . j = (Base_FinSeq (K,n,i)) . j by A12, A15, A17, A19; :: thesis: verum

end;

len P0 = n by MATRIX_1:def 3;
then i in Seg (len P0) by A15, A16, FINSEQ_1:3;
then i in dom P0 by FINSEQ_1:def 3;
then p in rng P0 by A17, FUNCT_1:def 5;
then A20: len p = n by MATRIX_1:def 3;
len (Base_FinSeq (K,n,i)) = n by Th23;
hence P0 . i = Base_FinSeq (K,n,i) by A17, A20, A18, FINSEQ_1:18; :: 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:25;
A23: len (Base_FinSeq (K,n,1)) = n by Th23;
A24: [1,1] in Indices P0 by A13, MATRIX_1:38;
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:25;
then A28: 1 in Seg (len P0) by A13, FINSEQ_1:3;
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:24;
k in Seg n by A30, A31, FINSEQ_1:3;
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:62
.= ((A * (1,1)) ") * (0. K) by A30, A31, A32, A35, Th25
.= 0. K by VECTSP_1:36 ; :: thesis: verum

end;

k in Seg n by A30, A31, FINSEQ_1:3;
then A36: k in dom P0 by A27, FINSEQ_1:def 3;

A37: now

k in Seg n by A30, A31, FINSEQ_1:3;
then [k,1] in Indices P0 by A27, A28, A22, ZFMISC_1:106;
then A38: ex p being FinSequence of K st
( p = P0 . k & P0 * (k,1) = p . 1 ) by MATRIX_1:def 6;
assume A39: k <> 1 ; :: thesis: (Col (P0,1)) . k = 0. K
then ( k in NAT & 1 < k ) by A30, ORDINAL1:def 13, 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 9; :: 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:62
.= ((A * (1,1)) ") * (1. K) by A31, A32, A41, Th24
.= (A * (1,1)) " by VECTSP_1:def 16 ;
:: thesis: verum

end;

1 <= n by A30, A31, XXREAL_0:2;
then 1 in dom P0 by A27, FINSEQ_3:27;
hence (Col (P0,1)) . k = (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k by A25, A34, A40, A37, MATRIX_1:def 9; :: thesis: verum

end;

A42: len A = n by MATRIX_1:25;
then A43: 1 in Seg (len A) by A3, FINSEQ_1:3;
then A44: 1 in dom A by FINSEQ_1:def 3;
A45: width A = n by MATRIX_1:25;
then A46: len (Line (A,1)) = n by MATRIX_1:def 8;
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:3;
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 9
.= n by MATRIX_1:25 ;
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:24;
k in dom P0 by A27, A56, A57, FINSEQ_3:27;
then A60: p . k = P0 * (k,1) by MATRIX_1:def 9;
k in dom (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) by A54, A56, A57, FINSEQ_3:27;
then A61: (((A * (1,1)) ") * (Base_FinSeq (K,n,1))) . k = ((A * (1,1)) ") * ((Base_FinSeq (K,n,1)) /. k) by A59, FVSUM_1:62;

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 16 ;
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:24;
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:36 ;
[k,1] in Indices P0 by A52, A56, A57, MATRIX_1:38;
then A65: ex p2 being FinSequence of K st
( p2 = P0 . k & P0 * (k,1) = p2 . 1 ) by MATRIX_1:def 6;
k in NAT by ORDINAL1:def 13;
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:25;
then A67: len (Line (A,i)) = n by MATRIX_1:def 8;
then A68: (Line (A,i)) /. 1 = (Line (A,i)) . 1 by A3, FINSEQ_4:24
.= A * (i,1) by A48, MATRIX_1:def 8 ;
[i,1] in Indices (A * P0) by A50, A52, MATRIX_1:38;
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:18
.= ((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:36 ;
:: 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:38;
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:3;
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:24;
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:62 ;
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:24;
k in dom P0 by A27, A78, A79, FINSEQ_3:27;
then A84: p . k = P0 * (k,j) by MATRIX_1:def 9;

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:24
.= (- (((A * (1,1)) ") * (A * (1,j)))) * (1. K) by A79, A83, A85, Th24
.= - (((A * (1,1)) ") * (A * (1,j))) by VECTSP_1:def 16 ;
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:24
.= 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:10; :: 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:38, ORDINAL1:def 13;
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:24;
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:36 ;
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:24;
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:24
.= 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:10; :: 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:24;
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:36 ;
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:24;
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:24
.= 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:10; :: thesis: verum

end;

end;

end;

end;

end;

A98: width A = n by MATRIX_1:25;
then A99: len (Line (A,1)) = n by MATRIX_1:def 8;
then A100: (Line (A,1)) /. 1 = (Line (A,1)) . 1 by A3, FINSEQ_4:24
.= A * (1,1) by A48, MATRIX_1:def 8 ;
A101: j in Seg n by A70, A71, FINSEQ_1:3;
A102: len (Col (P0,j)) = len P0 by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
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:18;
A104: (Line (A,1)) /. j = (Line (A,1)) . j by A70, A71, A99, FINSEQ_4:24
.= A * (1,j) by A101, A98, MATRIX_1:def 8 ;
[1,j] in Indices (A * P0) by A13, A70, A71, MATRIX_1:38;
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:41
.= (- ((A * (1,j)) * (((A * (1,1)) ") * (A * (1,1))))) + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by GROUP_1:def 4
.= (- ((A * (1,j)) * (1. K))) + |((Line (A,1)),(Base_FinSeq (K,n,j)))| by A2, VECTSP_1:def 22
.= (- ((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 16
.= 0. K by RLVECT_1:16 ;
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:25;
A106: len (Col (P0,1)) = len P0 by MATRIX_1:def 9
.= n by MATRIX_1:25 ;
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:18;
A108: len (((A * (1,1)) ") * (Line (A,1))) = len (Line (A,1)) by MATRIXR1:16
.= n by A45, MATRIX_1:def 8 ;
[1,1] in Indices A by A3, MATRIX_1:38;
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 2
.= (((A * (1,1)) ") * (Line (A,1))) . 1 by A3, A108, FINSEQ_4:24
.= ((A * (1,1)) ") * (A * (1,1)) by A48, A44, MATRIX12:3
.= 1. K by A2, VECTSP_1:def 22 ;
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