let K be Field; :: thesis:
let n be Element of NAT ; :: thesis:
let i0 be Nat; :: thesis:
let A be Matrix of n,K; :: thesis:
assume A1: ( 1 <= i0 & i0 <= n ) ; :: thesis:
assume A2: A = SwapDiagonal (K,n,i0) ; :: thesis:
let i, j be Nat; :: thesis:
assume that
A3: 1 <= i and
A4: i <= n and
A5: 1 <= j and
A6: j <= n ; :: thesis:
A7: [i,j] in Indices A by A3, A4, A5, A6, MATRIX_0:31;
assume A8: i0 <> 1 ; :: thesis:
thus ( i = 1 & j = i0 implies A * (i,j) = 1. K ) :: thesis:

reconsider j0 = i0 -' 2 as Element of NAT ;
reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
assume that
A9: i = 1 and
A10: j = i0 ; :: thesis:
reconsider qq = f /. i0 as FinSequence of the carrier of K by FINSEQ_1:def 11;
i0 <= len f by A6, A10, MATRIX_0:def 2;
then f /. i0 = f . i0 by A5, A10, FINSEQ_4:15
.= Base_FinSeq (K,n,i0) by A5, A6, A10, Th26 ;
then A11: qq . j = 1. K by A5, A6, A10, Th24;
reconsider g = f /^ 1 as FinSequence of the carrier of K * ;
A12: len f = n by MATRIX_0:def 2;
reconsider h = g | j0 as FinSequence of the carrier of K * ;
len (<*(f /. i0)*> ^ h) = (len <*(f /. i0)*>) + (len h) by FINSEQ_1:22
.= 1 + (len h) by FINSEQ_1:39 ;
then A13: 1 <= len (<*(f /. i0)*> ^ h) by NAT_1:11;
A14: 1 = len <*(f /. i0)*> by FINSEQ_1:39;
1 < i0 by A5, A8, A10, XXREAL_0:1;
then A . i = (((<*(f /. i0)*> ^ h) ^ <*(f /. 1)*>) ^ (f /^ i0)) . i by A2, A6, A10, A12, FINSEQ_7:28
.= ((<*(f /. i0)*> ^ h) ^ (<*(f /. 1)*> ^ (f /^ i0))) . i by FINSEQ_1:32
.= (<*(f /. i0)*> ^ h) . 1 by A9, A13, FINSEQ_1:64
.= <*(f /. i0)*> . 1 by A14, FINSEQ_1:64
.= f /. i0 ;
hence A * (i,j) = 1. K by A7, A11, MATRIX_0:def 5; :: thesis:

end;

A15: len A = n by MATRIX_0:24;
A16: 1 <= n by A3, A4, XXREAL_0:2;
thus ( i = i0 & j = 1 implies A * (i,j) = 1. K ) :: thesis:

reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
assume that
A17: i = i0 and
A18: j = 1 ; :: thesis:
reconsider qq = f /. 1 as FinSequence of the carrier of K by FINSEQ_1:def 11;
A19: len f = n by MATRIX_0:def 2;
then f /. 1 = f . 1 by A16, FINSEQ_4:15
.= Base_FinSeq (K,n,1) by A16, Th26 ;
then A20: qq . j = 1. K by A6, A18, Th24;
A . i = A /. i by A15, A3, A4, FINSEQ_4:15
.= f /. 1 by A2, A3, A4, A6, A17, A18, A19, FINSEQ_7:31 ;
hence A * (i,j) = 1. K by A7, A20, MATRIX_0:def 5; :: thesis:

end;

thus ( i = 1 & j = 1 implies A * (i,j) = 0. K ) :: thesis:

reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
assume that
A21: i = 1 and
A22: j = 1 ; :: thesis:
reconsider qq = f /. i0 as FinSequence of the carrier of K by FINSEQ_1:def 11;
A23: len f = n by MATRIX_0:def 2;
then f /. i0 = f . i0 by A1, FINSEQ_4:15
.= Base_FinSeq (K,n,i0) by A1, Th26 ;
then A24: qq . j = 0. K by A4, A8, A21, A22, Th25;
A . i = A /. i by A15, A3, A4, FINSEQ_4:15
.= f /. i0 by A1, A2, A4, A21, A23, FINSEQ_7:31 ;
hence A * (i,j) = 0. K by A7, A24, MATRIX_0:def 5; :: thesis:

end;

thus ( i = i0 & j = i0 implies A * (i,j) = 0. K ) :: thesis:

reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
assume that
A25: i = i0 and
A26: j = i0 ; :: thesis:
reconsider qq = f /. 1 as FinSequence of the carrier of K by FINSEQ_1:def 11;
A27: len f = n by MATRIX_0:def 2;
then f /. 1 = f . 1 by A16, FINSEQ_4:15
.= Base_FinSeq (K,n,1) by A16, Th26 ;
then A28: qq . j = 0. K by A1, A8, A26, Th25;
A . i = A /. i by A15, A3, A4, FINSEQ_4:15
.= f /. 1 by A2, A3, A4, A16, A25, A27, FINSEQ_7:31 ;
hence A * (i,j) = 0. K by A7, A28, MATRIX_0:def 5; :: thesis:

end;

assume A29: ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) ; :: thesis:

thus ( i = j implies A * (i,j) = 1. K ) :: thesis:

reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
assume A31: i = j ; :: thesis:
reconsider qq = f /. i as FinSequence of the carrier of K by FINSEQ_1:def 11;
j <= len f by A6, MATRIX_0:def 2;
then f /. i = f . i by A5, A31, FINSEQ_4:15
.= Base_FinSeq (K,n,i) by A3, A4, Th26 ;
then A32: qq . j = 1. K by A3, A4, A31, Th24;
A33: len f = n by MATRIX_0:def 2;
A . i = A /. i by A15, A3, A4, FINSEQ_4:15
.= f /. i by A2, A3, A4, A30, A33, FINSEQ_7:30 ;
hence A * (i,j) = 1. K by A7, A32, MATRIX_0:def 5; :: thesis:

end;

thus ( i <> j implies A * (i,j) = 0. K ) :: thesis:

reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
assume A34: i <> j ; :: thesis:
reconsider qq = f /. i as FinSequence of the carrier of K by FINSEQ_1:def 11;
A35: len f = n by MATRIX_0:def 2;
then f /. i = f . i by A3, A4, FINSEQ_4:15
.= Base_FinSeq (K,n,i) by A3, A4, Th26 ;
then A36: qq . j = 0. K by A5, A6, A34, Th25;
A . i = A /. i by A15, A3, A4, FINSEQ_4:15
.= f /. i by A2, A3, A4, A30, A35, FINSEQ_7:30 ;
hence A * (i,j) = 0. K by A7, A36, MATRIX_0:def 5; :: thesis:

end;

thus ( i = j implies A * (i,j) = 1. K ) :: thesis:

reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
assume A38: i = j ; :: thesis:
reconsider qq = f /. i as FinSequence of the carrier of K by FINSEQ_1:def 11;
j <= len f by A6, MATRIX_0:def 2;
then f /. i = f . i by A5, A38, FINSEQ_4:15
.= Base_FinSeq (K,n,i) by A3, A4, Th26 ;
then A39: qq . j = 1. K by A3, A4, A38, Th24;
A40: len f = n by MATRIX_0:def 2;
A . i = A /. i by A15, A3, A4, FINSEQ_4:15
.= f /. i by A2, A3, A4, A37, A38, A40, FINSEQ_7:30 ;
hence A * (i,j) = 1. K by A7, A39, MATRIX_0:def 5; :: thesis:

end;

thus ( i <> j implies A * (i,j) = 0. K ) :: thesis:

reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
reconsider qq = f /. i as FinSequence of the carrier of K by FINSEQ_1:def 11;
A43: len f = n by MATRIX_0:def 2;
then f /. i = f . i by A3, A4, FINSEQ_4:15
.= Base_FinSeq (K,n,i) by A3, A4, Th26 ;
then A44: qq . j = 0. K by A5, A6, A41, Th25;
A . i = A /. i by A15, A3, A4, FINSEQ_4:15
.= f /. i by A2, A3, A4, A42, A43, FINSEQ_7:30 ;
hence A * (i,j) = 0. K by A7, A44, MATRIX_0:def 5; :: thesis:

end;

reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
reconsider qq = f /. i0 as FinSequence of the carrier of K by FINSEQ_1:def 11;
A47: len f = n by MATRIX_0:def 2;
then f /. i0 = f . i0 by A1, FINSEQ_4:15
.= Base_FinSeq (K,n,i0) by A1, Th26 ;
then A48: qq . j = 0. K by A5, A6, A37, Th25;
A . i = A /. i by A15, A3, A4, FINSEQ_4:15
.= f /. i0 by A1, A2, A4, A46, A47, FINSEQ_7:31 ;
hence A * (i,j) = 0. K by A7, A48, MATRIX_0:def 5; :: thesis:

end;

reconsider f = 1. (K,n) as FinSequence of the carrier of K * ;
reconsider qq = f /. 1 as FinSequence of the carrier of K by FINSEQ_1:def 11;
A50: len f = n by MATRIX_0:def 2;
then f /. 1 = f . 1 by A16, FINSEQ_4:15
.= Base_FinSeq (K,n,1) by A16, Th26 ;
then A51: qq . j = 0. K by A5, A6, A37, Th25;
A . i = A /. i by A15, A3, A4, FINSEQ_4:15
.= f /. 1 by A2, A3, A4, A16, A49, A50, FINSEQ_7:31 ;
hence A * (i,j) = 0. K by A7, A51, MATRIX_0:def 5; :: thesis:

end;