let n be Element of NAT ; :: thesis:
let K be Field; :: thesis:
let a be Element of K; :: thesis:
let P be Matrix of n,K; :: thesis:
assume that
A1: n > 0 and
A2: ( a <> 0. K & P * (1,1) = a " & ( for i being Element of NAT st 1 < i & i <= n holds
P . i = Base_FinSeq (K,n,i) ) ) ; :: thesis:
defpred S₁[ Nat, Nat, Element of K] means ( ( $1 = 1 implies ( ( $2 = 1 implies $3 = a ) & ( $2 <> 1 implies $3 = - (a * (P * (1,$2))) ) ) ) & ( $1 <> 1 implies for i0 being Element of NAT st i0 = $1 holds
$3 = (Base_FinSeq (K,n,i0)) . $2 ) );
A3: 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]

let i, j be Nat; :: thesis:
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;
assume [i,j] in [:(Seg n),(Seg n):] ; :: thesis:
then j0 in Seg n by ZFMISC_1:87;
then A4: ( 1 <= j0 & j0 <= n ) by FINSEQ_1:1;

suppose A5: i = 1 ; :: thesis:

now :: thesis:

per cases ;

case A6: j = 1 ; :: thesis:

set x1 = a;
thus ( ( i = 1 implies ( ( j = 1 implies a = a ) & ( j <> 1 implies a = - (a * (P * (1,j))) ) ) ) & ( i <> 1 implies for i1 being Element of NAT st i1 = i holds
a = (Base_FinSeq (K,n,i1)) . j ) ) by A5, A6; :: thesis:

end;

case A7: j <> 1 ; :: thesis:

set x1 = - (a * (P * (1,j)));
thus ( ( i = 1 implies ( ( j = 1 implies - (a * (P * (1,j))) = a ) & ( j <> 1 implies - (a * (P * (1,j))) = - (a * (P * (1,j))) ) ) ) & ( i <> 1 implies for i1 being Element of NAT st i1 = i holds
- (a * (P * (1,j))) = (Base_FinSeq (K,n,i1)) . j ) ) by A5, A7; :: thesis:

end;

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

end;

suppose A8: i <> 1 ; :: thesis:

len (Base_FinSeq (K,n,i0)) = n by Th23;
then (Base_FinSeq (K,n,i0)) /. j0 = (Base_FinSeq (K,n,i0)) . j0 by A4, FINSEQ_4:15;
then reconsider x1 = (Base_FinSeq (K,n,i0)) . j0 as Element of K ;
( i <> 1 implies for i1 being Element of NAT st i1 = i holds
x1 = (Base_FinSeq (K,n,i1)) . j ) ;
hence ex x being Element of K st S₁[i,j,x] by A8; :: thesis:

end;

consider Q0 being Matrix of n,n,K such that
A9: for i, j being Nat st [i,j] in Indices Q0 holds
S₁[i,j,Q0 * (i,j)] from MATRIX_0:sch 2(A3);
A10: 0 + 1 <= n by A1, NAT_1:13;
A11: for j being Element of NAT st 1 < j & j <= n holds
Q0 * (1,j) = - (a * (P * (1,j)))

proof

let j be Element of NAT ; :: thesis:
assume that
A12: 1 < j and
A13: j <= n ; :: thesis:
[1,j] in Indices Q0 by A10, A12, A13, MATRIX_0:31;
hence Q0 * (1,j) = - (a * (P * (1,j))) by A9, A12; :: thesis:

end;

A14: ( Indices Q0 = [:(Seg n),(Seg n):] & 1 in Seg n ) by A10, FINSEQ_1:1, MATRIX_0:24;
A15: for i being Element of NAT st 1 < i & i <= n holds
Q0 . i = Base_FinSeq (K,n,i)

proof

let i be Element of NAT ; :: thesis:
assume that
A16: 1 < i and
A17: i <= n ; :: thesis:
i in Seg n by A16, A17, FINSEQ_1:1;
then [i,1] in Indices Q0 by A14, ZFMISC_1:87;
then consider p being FinSequence of K such that
A18: p = Q0 . i and
Q0 * (i,1) = p . 1 by MATRIX_0:def 5;
A19: for j being Nat st 1 <= j & j <= n holds
p . j = (Base_FinSeq (K,n,i)) . j

proof

let j be Nat; :: thesis:
assume ( 1 <= j & j <= n ) ; :: thesis:
then A20: [i,j] in Indices Q0 by A16, A17, MATRIX_0:31;
then ex p2 being FinSequence of K st
( p2 = Q0 . i & Q0 * (i,j) = p2 . j ) by MATRIX_0:def 5;
hence p . j = (Base_FinSeq (K,n,i)) . j by A9, A16, A18, A20; :: thesis:

end;

len Q0 = n by MATRIX_0:def 2;
then i in Seg (len Q0) by A16, A17, FINSEQ_1:1;
then i in dom Q0 by FINSEQ_1:def 3;
then p in rng Q0 by A18, FUNCT_1:def 3;
then A21: len p = n by MATRIX_0:def 2;
len (Base_FinSeq (K,n,i)) = n by Th23;
hence Q0 . i = Base_FinSeq (K,n,i) by A18, A21, A19, FINSEQ_1:14; :: thesis:

end;

[1,1] in Indices Q0 by A10, MATRIX_0:31;
then Q0 * (1,1) = a by A9;
hence P is invertible by A1, A2, A11, A15, Th37; :: thesis: