let n be Element of NAT ; :: thesis: for K being Field
for a being Element of K
for P, Q being Matrix of n,K st n > 0 & 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) ) & Q * (1,1) = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * (1,j) = - (a * (P * (1,j))) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq (K,n,i) ) holds
( P is invertible & Q = P ~ )
let K be Field; :: thesis: for a being Element of K
for P, Q being Matrix of n,K st n > 0 & 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) ) & Q * (1,1) = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * (1,j) = - (a * (P * (1,j))) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq (K,n,i) ) holds
( P is invertible & Q = P ~ )
let a be Element of K; :: thesis: for P, Q being Matrix of n,K st n > 0 & 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) ) & Q * (1,1) = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * (1,j) = - (a * (P * (1,j))) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq (K,n,i) ) holds
( P is invertible & Q = P ~ )
let P, Q be Matrix of n,K; :: thesis: ( n > 0 & 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) ) & Q * (1,1) = a & ( for j being Element of NAT st 1 < j & j <= n holds
Q * (1,j) = - (a * (P * (1,j))) ) & ( for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq (K,n,i) ) implies ( P is invertible & Q = P ~ ) )
assume that
A1: n > 0 and
A2: a <> 0. K and
A3: P * (1,1) = a " and
A4: for i being Element of NAT st 1 < i & i <= n holds
P . i = Base_FinSeq (K,n,i) and
A5: Q * (1,1) = a and
A6: for j being Element of NAT st 1 < j & j <= n holds
Q * (1,j) = - (a * (P * (1,j))) and
A7: for i being Element of NAT st 1 < i & i <= n holds
Q . i = Base_FinSeq (K,n,i) ; :: thesis: ( P is invertible & Q = P ~ )
A8: 0 + 1 <= n by A1, NAT_1:13;
A9: len (Base_FinSeq (K,n,1)) = n by Th23;
A10: len P = n by MATRIX_0:24;
A11: len ((a ") * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A12: for k being Nat st 1 <= k & k <= n holds
(Col (P,1)) . k = ((a ") * (Base_FinSeq (K,n,1))) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies (Col (P,1)) . k = ((a ") * (Base_FinSeq (K,n,1))) . k )
A13: k in NAT by ORDINAL1:def 12;
assume that
A14: 1 <= k and
A15: k <= n ; :: thesis: (Col (P,1)) . k = ((a ") * (Base_FinSeq (K,n,1))) . k
A16: k in Seg n by A14, A15, FINSEQ_1:1;
then A17: k in dom P by A10, FINSEQ_1:def 3;

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

[k,1] in Indices P by A8, A14, A15, MATRIX_0:31;
then A19: ex p being FinSequence of K st
( p = P . k & P * (k,1) = p . 1 ) by MATRIX_0:def 5;
assume A20: k <> 1 ; :: thesis: (Col (P,1)) . k = 0. K
then 1 < k by A14, XXREAL_0:1;
then P * (k,1) = (Base_FinSeq (K,n,k)) . 1 by A4, A13, A15, A19
.= 0. K by A8, A20, Th25 ;
hence (Col (P,1)) . k = 0. K by A17, MATRIX_0:def 8; :: thesis: verum

end;

A21: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A9, A14, A15, FINSEQ_4:15;

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

assume A23: k = 1 ; :: thesis: ((a ") * (Base_FinSeq (K,n,1))) . k = a "
k in dom ((a ") * (Base_FinSeq (K,n,1))) by A11, A16, FINSEQ_1:def 3;
hence ((a ") * (Base_FinSeq (K,n,1))) . k = (a ") * ((Base_FinSeq (K,n,1)) /. k) by A21, FVSUM_1:50
.= (a ") * (1. K) by A15, A21, A23, Th24
.= a " ;
:: thesis: verum

end;

A24: k in dom ((a ") * (Base_FinSeq (K,n,1))) by A11, A14, A15, FINSEQ_3:25;

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

assume A26: k <> 1 ; :: thesis: ((a ") * (Base_FinSeq (K,n,1))) . k = 0. K
thus ((a ") * (Base_FinSeq (K,n,1))) . k = (a ") * ((Base_FinSeq (K,n,1)) /. k) by A24, A21, FVSUM_1:50
.= (a ") * (0. K) by A14, A15, A21, A26, Th25
.= 0. K ; :: thesis: verum

end;

1 <= n by A14, A15, XXREAL_0:2;
then 1 in dom P by A10, FINSEQ_3:25;
hence (Col (P,1)) . k = ((a ") * (Base_FinSeq (K,n,1))) . k by A3, A25, A22, A18, MATRIX_0:def 8; :: thesis: verum

end;

A27: 0 + 1 <= n by A1, NAT_1:13;
A28: len Q = n by MATRIX_0:24;
then A29: 1 in Seg (len Q) by A27, FINSEQ_1:1;
then A30: 1 in dom Q by FINSEQ_1:def 3;
A31: width Q = n by MATRIX_0:24;
then A32: len (Line (Q,1)) = n by MATRIX_0:def 7;
then A33: 1 in dom (Line (Q,1)) by A28, A29, FINSEQ_1:def 3;
A34: for j being Element of NAT st 1 < j & j <= n holds
P * (1,j) = - ((a ") * (Q * (1,j)))

proof

let j be Element of NAT ; :: thesis: ( 1 < j & j <= n implies P * (1,j) = - ((a ") * (Q * (1,j))) )
assume ( 1 < j & j <= n ) ; :: thesis: P * (1,j) = - ((a ") * (Q * (1,j)))
then - ((a ") * (Q * (1,j))) = - ((a ") * (- (a * (P * (1,j))))) by A6;
then - ((a ") * (Q * (1,j))) = - ((a ") * ((- a) * (P * (1,j)))) by VECTSP_1:9;
then - ((a ") * (Q * (1,j))) = (- (a ")) * ((- a) * (P * (1,j))) by VECTSP_1:9;
then - ((a ") * (Q * (1,j))) = ((- (a ")) * (- a)) * (P * (1,j)) by GROUP_1:def 3;
then - ((a ") * (Q * (1,j))) = (a * (a ")) * (P * (1,j)) by VECTSP_1:10;
then - ((a ") * (Q * (1,j))) = (1. K) * (P * (1,j)) by A2, VECTSP_1:def 10;
hence P * (1,j) = - ((a ") * (Q * (1,j))) ; :: thesis: verum

end;

A35: for j being Element of NAT st 1 < j & j <= n holds
(Q * P) * (1,j) = 0. K

proof

let j be Element of NAT ; :: thesis: ( 1 < j & j <= n implies (Q * P) * (1,j) = 0. K )
assume that
A36: 1 < j and
A37: j <= n ; :: thesis: (Q * P) * (1,j) = 0. K
A38: len (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) = len ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) by Th6
.= len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A39: j in Seg n by A36, A37, FINSEQ_1:1;
A40: 1 <= n by A36, A37, XXREAL_0:2;
then A41: 1 in Seg (width Q) by A31, FINSEQ_1:1;
len (Line (Q,1)) = n by A31, MATRIX_0:def 7;
then A42: (Line (Q,1)) /. j = (Line (Q,1)) . j by A36, A37, FINSEQ_4:15;
A43: (Line (Q,1)) /. 1 = (Line (Q,1)) . 1 by A32, A40, FINSEQ_4:15
.= a by A5, A41, MATRIX_0:def 7 ;
A44: len (Col (P,j)) = len P by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
reconsider p = Col (P,j), q = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) as FinSequence of K ;
A45: len (Base_FinSeq (K,n,j)) = n by Th23;
A46: len ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A47: for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

A48: len ((- ((a ") * (Q * (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
A49: 1 <= k and
A50: k <= n ; :: thesis: p . k = q . k
A51: k in dom ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) by A46, A49, A50, FINSEQ_3:25;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A52: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A49, A50, FINSEQ_4:15;
k in dom P by A10, A49, A50, FINSEQ_3:25;
then A53: p . k = P * (k,j) by MATRIX_0:def 8;
A54: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k = ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) . k by Th6
.= (- ((a ") * (Q * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A51, A52, FVSUM_1:50 ;

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

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

then 1 <= len (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) by A50, A48, Th6;
then A56: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) /. 1 = (- ((a ") * (Q * (1,j)))) * ((Base_FinSeq (K,n,1)) /. 1) by A54, A55, FINSEQ_4:15
.= (- ((a ") * (Q * (1,j)))) * (1. K) by A27, A52, A55, Th24
.= - ((a ") * (Q * (1,j))) ;
A57: p . 1 = - ((a ") * (Q * (1,j))) by A34, A36, A37, A53, A55;
(Base_FinSeq (K,n,j)) /. 1 = (Base_FinSeq (K,n,j)) . 1 by A45, A50, A55, FINSEQ_4:15
.= 0. K by A36, A50, A55, Th25 ;
then q . 1 = (- ((a ") * (Q * (1,j)))) + (0. K) by A38, A45, A50, A55, A56, Th5;
hence p . k = q . k by A55, A57, RLVECT_1:4; :: thesis: verum

end;

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

[k,j] in Indices P by A36, A37, A49, A50, MATRIX_0:31;
then A59: ex p2 being FinSequence of K st
( p2 = P . k & P * (k,j) = p2 . j ) by MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then A60: p . k = (Base_FinSeq (K,n,k)) . j by A4, A50, A53, A58, A59;

now :: thesis: p . k = q . k

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

suppose A61: 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 A49, A50, FINSEQ_4:15;
then A62: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- ((a ") * (Q * (1,j)))) * (0. K) by A50, A54, A58, Th25
.= 0. K ;
A63: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A38, A49, A50, FINSEQ_4:15;
A64: p . k = 0. K by A36, A37, A60, A61, Th25;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A45, A49, A50, FINSEQ_4:15
.= 0. K by A49, A50, A61, Th25 ;
then q . k = (0. K) + (0. K) by A38, A45, A49, A50, A63, A62, Th5;
hence p . k = q . k by A64, RLVECT_1:4; :: thesis: verum

end;

suppose A65: k = j ; :: thesis: p . k = q . k

then A66: p . k = 1. K by A49, A50, A60, Th24;
A67: (- (((a ") * (Q * (1,k))) * (Base_FinSeq (K,n,1)))) /. k = (- (((a ") * (Q * (1,k))) * (Base_FinSeq (K,n,1)))) . k by A38, A49, A50, A65, FINSEQ_4:15;
len (Base_FinSeq (K,n,1)) = n by Th23;
then (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A49, A50, FINSEQ_4:15;
then A68: (- (((a ") * (Q * (1,k))) * (Base_FinSeq (K,n,1)))) . k = (- ((a ") * (Q * (1,k)))) * (0. K) by A50, A54, A58, A65, Th25
.= 0. K ;
(Base_FinSeq (K,n,k)) /. k = (Base_FinSeq (K,n,k)) . k by A45, A49, A50, A65, FINSEQ_4:15
.= 1. K by A36, A37, A65, Th24 ;
then q . k = (0. K) + (1. K) by A38, A45, A49, A50, A65, A67, A68, Th5;
hence p . k = q . k by A66, RLVECT_1:4; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

len ((- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j))) = n by A38, A45, Th2;
then A69: Col (P,j) = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) by A44, A47, FINSEQ_1:14;
[1,j] in Indices (Q * P) by A27, A36, A37, MATRIX_0:31;
then (Q * P) * (1,j) = |((Line (Q,1)),(Col (P,j)))| by A10, A31, MATRIX_3:def 4
.= |((Line (Q,1)),(- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))))| + |((Line (Q,1)),(Base_FinSeq (K,n,j)))| by A32, A38, A45, A69, Th11
.= |((Line (Q,1)),((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))))| + |((Line (Q,1)),(Base_FinSeq (K,n,j)))| by Th6
.= ((- ((a ") * (Q * (1,j)))) * |((Line (Q,1)),(Base_FinSeq (K,n,1)))|) + |((Line (Q,1)),(Base_FinSeq (K,n,j)))| by A32, A9, Th10
.= ((- ((a ") * (Q * (1,j)))) * a) + |((Line (Q,1)),(Base_FinSeq (K,n,j)))| by A32, A27, A43, Th35
.= (- (((a ") * (Q * (1,j))) * a)) + |((Line (Q,1)),(Base_FinSeq (K,n,j)))| by VECTSP_1:9
.= (- ((Q * (1,j)) * ((a ") * a))) + |((Line (Q,1)),(Base_FinSeq (K,n,j)))| by GROUP_1:def 3
.= (- ((Q * (1,j)) * (1. K))) + |((Line (Q,1)),(Base_FinSeq (K,n,j)))| by A2, VECTSP_1:def 10
.= (- ((Q * (1,j)) * (1. K))) + ((Line (Q,1)) /. j) by A32, A36, A37, Th35
.= (- (Q * (1,j))) + ((Line (Q,1)) /. j)
.= (- (Q * (1,j))) + (Q * (1,j)) by A31, A39, A42, MATRIX_0:def 7
.= 0. K by RLVECT_1:5 ;
hence (Q * P) * (1,j) = 0. K ; :: thesis: verum

end;

A70: 1 in Seg (width Q) by A31, A27, FINSEQ_1:1;
A71: for i, j being Element of NAT st 1 < i & i <= n & i = j holds
(Q * P) * (i,j) = 1. K

proof

let i, j be Element of NAT ; :: thesis: ( 1 < i & i <= n & i = j implies (Q * P) * (i,j) = 1. K )
assume that
A72: 1 < i and
A73: i <= n and
A74: i = j ; :: thesis: (Q * P) * (i,j) = 1. K
A75: len (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) = len ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) by Th6
.= len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
[i,j] in Indices Q by A72, A73, A74, MATRIX_0:31;
then consider p1 being FinSequence of K such that
A76: p1 = Q . i and
A77: Q * (i,j) = p1 . j by MATRIX_0:def 5;
p1 = Base_FinSeq (K,n,i) by A7, A72, A73, A76;
then A78: p1 . j = 1. K by A72, A73, A74, Th24;
[i,1] in Indices Q by A8, A72, A73, MATRIX_0:31;
then consider p2 being FinSequence of K such that
A79: p2 = Q . i and
A80: Q * (i,1) = p2 . 1 by MATRIX_0:def 5;
A81: width Q = n by MATRIX_0:24;
A82: j in Seg n by A72, A73, A74, FINSEQ_1:1;
A83: len (Col (P,j)) = len P by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
reconsider p = Col (P,j), q = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) as FinSequence of K ;
A84: len (Base_FinSeq (K,n,j)) = n by Th23;
A85: len ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A86: for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

A87: len ((- ((a ") * (Q * (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
A88: 1 <= k and
A89: k <= n ; :: thesis: p . k = q . k
k in Seg n by A88, A89, FINSEQ_1:1;
then A90: k in dom ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) by A85, FINSEQ_1:def 3;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A91: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A88, A89, FINSEQ_4:15;
k in dom P by A10, A88, A89, FINSEQ_3:25;
then A92: p . k = P * (k,j) by MATRIX_0:def 8;
A93: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k = ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) . k by Th6
.= (- ((a ") * (Q * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A90, A91, FVSUM_1:50 ;

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

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

k <= len (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) by A89, A87, Th6;
then A95: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- ((a ") * (Q * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A88, A93, FINSEQ_4:15
.= (- ((a ") * (Q * (1,j)))) * (1. K) by A27, A91, A94, Th24
.= - ((a ") * (Q * (1,j))) ;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A84, A88, A89, FINSEQ_4:15
.= 0. K by A72, A74, A89, A94, Th25 ;
then A96: q . k = (- ((a ") * (Q * (1,j)))) + (0. K) by A75, A84, A88, A89, A95, Th5;
p . k = - ((a ") * (Q * (1,j))) by A34, A72, A73, A74, A92, A94;
hence p . k = q . k by A96, RLVECT_1:4; :: thesis: verum

end;

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

[k,j] in Indices P by A72, A73, A74, A88, A89, MATRIX_0:31;
then A98: ex p2 being FinSequence of K st
( p2 = P . k & P * (k,j) = p2 . j ) by MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then A99: p . k = (Base_FinSeq (K,n,k)) . j by A4, A89, A92, A97, A98;

now :: thesis: p . k = q . k

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

suppose A100: 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 A88, A89, FINSEQ_4:15;
then A101: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- ((a ") * (Q * (1,j)))) * (0. K) by A89, A93, A97, Th25
.= 0. K ;
A102: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A75, A88, A89, FINSEQ_4:15;
A103: p . k = 0. K by A72, A73, A74, A99, A100, Th25;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A84, A88, A89, FINSEQ_4:15
.= 0. K by A88, A89, A100, Th25 ;
then q . k = (0. K) + (0. K) by A75, A84, A88, A89, A102, A101, Th5;
hence p . k = q . k by A103, RLVECT_1:4; :: thesis: verum

end;

suppose A104: 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 A88, A89, FINSEQ_4:15;
then A105: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- ((a ") * (Q * (1,j)))) * (0. K) by A89, A93, A97, Th25
.= 0. K ;
A106: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A75, A88, A89, FINSEQ_4:15;
A107: p . k = 1. K by A88, A89, A99, A104, Th24;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A84, A88, A89, FINSEQ_4:15
.= 1. K by A88, A89, A104, Th24 ;
then q . k = (0. K) + (1. K) by A75, A84, A88, A89, A106, A105, Th5;
hence p . k = q . k by A107, RLVECT_1:4; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

len ((- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j))) = n by A75, A84, Th2;
then A108: Col (P,j) = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) by A83, A86, FINSEQ_1:14;
A109: len (Line (Q,i)) = n by A31, MATRIX_0:def 7;
then A110: (Line (Q,i)) /. 1 = (Line (Q,i)) . 1 by A27, FINSEQ_4:15
.= Q * (i,1) by A70, MATRIX_0:def 7 ;
A111: (Line (Q,i)) /. j = (Line (Q,i)) . j by A72, A73, A74, A109, FINSEQ_4:15
.= Q * (i,j) by A82, A81, MATRIX_0:def 7 ;
[i,j] in Indices (Q * P) by A72, A73, A74, MATRIX_0:31;
then A112: (Q * P) * (i,j) = |((Line (Q,i)),(Col (P,j)))| by A10, A81, MATRIX_3:def 4
.= |((Line (Q,i)),(- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))))| + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by A75, A84, A108, A109, Th11
.= |((Line (Q,i)),((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))))| + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by Th6
.= ((- ((a ") * (Q * (1,j)))) * |((Line (Q,i)),(Base_FinSeq (K,n,1)))|) + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by A9, A109, Th10
.= ((- ((a ") * (Q * (1,j)))) * (Q * (i,1))) + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by A27, A109, A110, Th35
.= (- (((Q * (1,j)) * (a ")) * (Q * (i,1)))) + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by VECTSP_1:9
.= (- ((Q * (1,j)) * ((a ") * (Q * (i,1))))) + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by GROUP_1:def 3
.= (- ((Q * (1,j)) * ((a ") * (Q * (i,1))))) + (Q * (i,j)) by A72, A73, A74, A109, A111, Th35 ;
A113: 1 <= n by A72, A73, XXREAL_0:2;
p2 = Base_FinSeq (K,n,i) by A7, A72, A73, A79;
hence (Q * P) * (i,j) = (- ((Q * (1,j)) * ((a ") * (0. K)))) + (Q * (i,j)) by A72, A113, A112, A80, Th25
.= (- ((Q * (1,j)) * (0. K))) + (Q * (i,j))
.= (- (0. K)) + (Q * (i,j))
.= (0. K) + (1. K) by A77, A78, RLVECT_1:12
.= 1. K by RLVECT_1:4 ;
:: thesis: verum

end;

A114: Indices P = [:(Seg n),(Seg n):] by MATRIX_0:24;
A115: for i, j being Element of NAT st 1 < i & i <= n & 1 <= j & j <= n & i <> j holds
(Q * P) * (i,j) = 0. K

proof

A116: len ((a ") * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
let i, j be Element of NAT ; :: thesis: ( 1 < i & i <= n & 1 <= j & j <= n & i <> j implies (Q * P) * (i,j) = 0. K )
assume that
A117: 1 < i and
A118: i <= n and
A119: 1 <= j and
A120: j <= n and
A121: i <> j ; :: thesis: (Q * P) * (i,j) = 0. K
A122: [i,j] in Indices (Q * P) by A117, A118, A119, A120, MATRIX_0:31;
A123: j in Seg n by A119, A120, FINSEQ_1:1;
A124: len ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A125: len (Col (P,j)) = len P by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
A126: [i,1] in Indices Q by A27, A117, A118, MATRIX_0:31;
A127: len (Base_FinSeq (K,n,j)) = n by Th23;
A128: len (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) = len ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) by Th6
.= len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
then A129: len ((- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j))) = n by A127, Th2;
A130: [i,j] in Indices Q by A117, A118, A119, A120, MATRIX_0:31;

now :: thesis: (Q * P) * (i,j) = 0. K

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

suppose A131: j > 1 ; :: thesis: (Q * P) * (i,j) = 0. K

reconsider p = Col (P,j), q = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) as FinSequence of K ;
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
A132: 1 <= k and
A133: k <= n ; :: thesis: p . k = q . k
k in Seg n by A132, A133, FINSEQ_1:1;
then A134: k in dom ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) by A124, FINSEQ_1:def 3;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A135: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A132, A133, FINSEQ_4:15;
k in dom P by A10, A132, A133, FINSEQ_3:25;
then A136: p . k = P * (k,j) by MATRIX_0:def 8;
A137: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k = ((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))) . k by Th6
.= (- ((a ") * (Q * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A134, A135, FVSUM_1:50 ;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A138: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A132, A133, FINSEQ_4:15;

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

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

then A140: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- ((a ") * (Q * (1,j)))) * (1. K) by A27, A135, A137, Th24;
A141: (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A128, A132, A133, FINSEQ_4:15;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A127, A132, A133, FINSEQ_4:15
.= 0. K by A131, A133, A139, Th25 ;
then q . k = ((- ((a ") * (Q * (1,j)))) * (1. K)) + (0. K) by A128, A127, A132, A133, A141, A140, Th5
.= (- ((a ") * (Q * (1,j)))) * (1. K) by RLVECT_1:4
.= - ((a ") * (Q * (1,j))) ;
hence p . k = q . k by A34, A120, A131, A136, A139; :: thesis: verum

end;

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

[k,j] in Indices P by A119, A120, A132, A133, MATRIX_0:31;
then A143: ex p2 being FinSequence of K st
( p2 = P . k & P * (k,j) = p2 . j ) by MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then A144: p . k = (Base_FinSeq (K,n,k)) . j by A4, A133, A136, A142, A143;

now :: thesis: p . k = q . k

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

suppose A145: k <> j ; :: thesis: p . k = q . k

(- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- ((a ") * (Q * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A128, A132, A133, A137, FINSEQ_4:15
.= (- ((a ") * (Q * (1,j)))) * (0. K) by A133, A138, A142, Th25
.= 0. K ;
then q . k = (0. K) + ((Base_FinSeq (K,n,j)) /. k) by A128, A127, A132, A133, Th5
.= (Base_FinSeq (K,n,j)) /. k by RLVECT_1:4
.= (Base_FinSeq (K,n,j)) . k by A127, A132, A133, FINSEQ_4:15
.= 0. K by A132, A133, A145, Th25 ;
hence p . k = q . k by A119, A120, A144, A145, Th25; :: thesis: verum

end;

suppose A146: k = j ; :: thesis: p . k = q . k

(- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- ((a ") * (Q * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A128, A132, A133, A137, FINSEQ_4:15
.= (- ((a ") * (Q * (1,j)))) * (0. K) by A133, A138, A142, Th25
.= 0. K ;
then q . k = (0. K) + ((Base_FinSeq (K,n,j)) /. k) by A128, A127, A132, A133, Th5
.= (Base_FinSeq (K,n,j)) /. k by RLVECT_1:4
.= (Base_FinSeq (K,n,j)) . k by A127, A132, A133, FINSEQ_4:15
.= 1. K by A119, A120, A146, Th24 ;
hence p . k = q . k by A132, A133, A144, A146, Th24; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

then A147: Col (P,j) = (- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) by A125, A129, FINSEQ_1:14;
A148: 1 <= n by A117, A118, XXREAL_0:2;
A149: width Q = n by MATRIX_0:24;
then A150: len (Line (Q,i)) = n by MATRIX_0:def 7;
then A151: (Line (Q,i)) /. j = (Line (Q,i)) . j by A119, A120, FINSEQ_4:15
.= Q * (i,j) by A123, A149, MATRIX_0:def 7 ;
A152: (Line (Q,i)) /. 1 = (Line (Q,i)) . 1 by A27, A150, FINSEQ_4:15
.= Q * (i,1) by A70, MATRIX_0:def 7 ;
A153: (Q * P) * (i,j) = |((Line (Q,i)),(Col (P,j)))| by A10, A122, A149, MATRIX_3:def 4
.= |((Line (Q,i)),(- (((a ") * (Q * (1,j))) * (Base_FinSeq (K,n,1)))))| + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by A128, A127, A147, A150, Th11
.= |((Line (Q,i)),((- ((a ") * (Q * (1,j)))) * (Base_FinSeq (K,n,1))))| + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by Th6
.= ((- ((a ") * (Q * (1,j)))) * |((Line (Q,i)),(Base_FinSeq (K,n,1)))|) + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by A9, A150, Th10
.= ((- ((a ") * (Q * (1,j)))) * (Q * (i,1))) + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by A27, A150, A152, Th35
.= (- (((Q * (1,j)) * (a ")) * (Q * (i,1)))) + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by VECTSP_1:9
.= (- ((Q * (1,j)) * ((a ") * (Q * (i,1))))) + |((Line (Q,i)),(Base_FinSeq (K,n,j)))| by GROUP_1:def 3
.= (- ((Q * (1,j)) * ((a ") * (Q * (i,1))))) + (Q * (i,j)) by A119, A120, A150, A151, Th35 ;
consider p2 being FinSequence of K such that
A154: p2 = Q . i and
A155: Q * (i,1) = p2 . 1 by A126, MATRIX_0:def 5;
consider p1 being FinSequence of K such that
A156: p1 = Q . i and
A157: Q * (i,j) = p1 . j by A130, MATRIX_0:def 5;
p1 = Base_FinSeq (K,n,i) by A7, A117, A118, A156;
then A158: p1 . j = 0. K by A119, A120, A121, Th25;
p2 = Base_FinSeq (K,n,i) by A7, A117, A118, A154;
hence (Q * P) * (i,j) = (- ((Q * (1,j)) * ((a ") * (0. K)))) + (Q * (i,j)) by A117, A148, A153, A155, Th25
.= (- ((Q * (1,j)) * (0. K))) + (Q * (i,j))
.= (- (0. K)) + (Q * (i,j))
.= (0. K) + (0. K) by A157, A158, RLVECT_1:12
.= 0. K by RLVECT_1:4 ;
:: thesis: verum

end;

suppose A159: j <= 1 ; :: thesis: (Q * P) * (i,j) = 0. K

reconsider p = Col (P,j), q = (a ") * (Base_FinSeq (K,n,1)) as FinSequence of K ;
A160: 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
A161: 1 <= k and
A162: k <= n ; :: thesis: p . k = q . k
A163: len (Base_FinSeq (K,n,1)) = n by Th23;
then A164: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A161, A162, FINSEQ_4:15;
A165: k in Seg n by A161, A162, FINSEQ_1:1;
then k in dom ((a ") * (Base_FinSeq (K,n,1))) by A116, FINSEQ_1:def 3;
then A166: ((a ") * (Base_FinSeq (K,n,1))) . k = (a ") * ((Base_FinSeq (K,n,1)) /. k) by A164, FVSUM_1:50;
k in dom P by A10, A161, A162, FINSEQ_3:25;
then A167: p . k = P * (k,j) by MATRIX_0:def 8;

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

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

then q . k = (a ") * (1. K) by A162, A164, A166, Th24
.= a " ;
hence p . k = q . k by A3, A119, A159, A167, A168, XXREAL_0:1; :: thesis: verum

end;

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

[k,j] in Indices P by A114, A123, A165, ZFMISC_1:87;
then A170: ex p2 being FinSequence of K st
( p2 = P . k & P * (k,j) = p2 . j ) by MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then A171: p . k = (Base_FinSeq (K,n,k)) . j by A4, A162, A167, A169, A170;

now :: thesis: p . k = q . k

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

suppose A172: k <> j ; :: thesis: p . k = q . k

(Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A161, A162, A163, FINSEQ_4:15;
then (a ") * ((Base_FinSeq (K,n,1)) /. k) = (a ") * (0. K) by A162, A169, Th25
.= 0. K ;
hence p . k = q . k by A119, A120, A166, A171, A172, Th25; :: thesis: verum

end;

suppose k = j ; :: thesis: p . k = q . k

hence p . k = q . k by A159, A169; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

A173: 1 <= n by A117, A118, XXREAL_0:2;
A174: width Q = n by MATRIX_0:24;
then A175: len (Line (Q,i)) = n by MATRIX_0:def 7;
then A176: (Line (Q,i)) /. 1 = (Line (Q,i)) . 1 by A27, FINSEQ_4:15
.= Q * (i,1) by A70, MATRIX_0:def 7 ;
A177: (Q * P) * (i,j) = |((Line (Q,i)),(Col (P,j)))| by A10, A122, A174, MATRIX_3:def 4
.= |((Line (Q,i)),((a ") * (Base_FinSeq (K,n,1))))| by A125, A116, A160, FINSEQ_1:14
.= (a ") * |((Line (Q,i)),(Base_FinSeq (K,n,1)))| by A9, A175, Th10
.= (a ") * (Q * (i,1)) by A27, A175, A176, Th35 ;
consider p2 being FinSequence of K such that
A178: p2 = Q . i and
A179: Q * (i,1) = p2 . 1 by A126, MATRIX_0:def 5;
p2 = Base_FinSeq (K,n,i) by A7, A117, A118, A178;
hence (Q * P) * (i,j) = (a ") * (0. K) by A117, A173, A177, A179, Th25
.= 0. K ;
:: thesis: verum

end;

end;

end;

hence (Q * P) * (i,j) = 0. K ; :: thesis: verum

end;

len (Col (P,1)) = len P by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
then A180: Col (P,1) = (a ") * (Base_FinSeq (K,n,1)) by A11, A12, FINSEQ_1:14;
A181: Indices (Q * P) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A182: len ((a ") * (Line (Q,1))) = len (Line (Q,1)) by MATRIXR1:16
.= n by A31, MATRIX_0:def 7 ;
( Indices Q = [:(Seg n),(Seg n):] & [1,1] in Indices Q ) by A27, MATRIX_0:24, MATRIX_0:31;
then A183: (Q * P) * (1,1) = |((Line (Q,1)),(Col (P,1)))| by A10, A31, A181, MATRIX_3:def 4
.= (a ") * |((Line (Q,1)),(Base_FinSeq (K,n,1)))| by A32, A9, A180, Th10
.= (a ") * ((Line (Q,1)) /. 1) by A32, A27, Th35
.= ((a ") * (Line (Q,1))) /. 1 by A33, POLYNOM1:def 1
.= ((a ") * (Line (Q,1))) . 1 by A27, A182, FINSEQ_4:15
.= (a ") * (Q * (1,1)) by A70, A30, MATRIX12:3
.= 1. K by A2, A5, VECTSP_1:def 10 ;
for i, j being Nat st [i,j] in Indices (Q * P) holds
(Q * P) * (i,j) = (1. (K,n)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (Q * P) implies (Q * P) * (i,j) = (1. (K,n)) * (i,j) )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;
assume A184: [i,j] in Indices (Q * P) ; :: thesis: (Q * P) * (i,j) = (1. (K,n)) * (i,j)
then A185: i in Seg n by A181, ZFMISC_1:87;
then A186: 1 <= i by FINSEQ_1:1;
A187: i <= n by A185, FINSEQ_1:1;
A188: j in Seg n by A181, A184, ZFMISC_1:87;
then A189: 1 <= j by FINSEQ_1:1;
A190: j <= n by A188, FINSEQ_1:1;

per cases ( 1 < i or 1 = i ) by A186, XXREAL_0:1;

suppose A191: 1 < i ; :: thesis: (Q * P) * (i,j) = (1. (K,n)) * (i,j)

now :: thesis: (Q * P) * (i,j) = (1. (K,n)) * (i,j)

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

suppose A192: i <> j ; :: thesis: (Q * P) * (i,j) = (1. (K,n)) * (i,j)

A193: (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i0)) . j0 by A186, A187, A189, A190, Th27
.= 0. K by A189, A190, A192, Th25 ;
thus (Q * P) * (i,j) = (Q * P) * (i0,j0)
.= (1. (K,n)) * (i,j) by A115, A187, A189, A190, A191, A192, A193 ; :: thesis: verum

end;

suppose A194: i = j ; :: thesis: (Q * P) * (i,j) = (1. (K,n)) * (i,j)

A195: (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i0)) . j0 by A186, A187, A189, A190, Th27
.= 1. K by A189, A190, A194, Th24 ;
thus (Q * P) * (i,j) = (Q * P) * (i0,j0)
.= (1. (K,n)) * (i,j) by A71, A190, A191, A194, A195 ; :: thesis: verum

end;

end;

end;

hence (Q * P) * (i,j) = (1. (K,n)) * (i,j) ; :: thesis: verum

end;

suppose A196: 1 = i ; :: thesis: (Q * P) * (i,j) = (1. (K,n)) * (i,j)

now :: thesis: (Q * P) * (i,j) = (1. (K,n)) * (i,j)

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

suppose A197: i < j ; :: thesis: (Q * P) * (i,j) = (1. (K,n)) * (i,j)

A198: (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i0)) . j0 by A186, A187, A189, A190, Th27
.= 0. K by A189, A190, A197, Th25 ;
thus (Q * P) * (i,j) = (Q * P) * (i0,j0)
.= (1. (K,n)) * (i,j) by A35, A190, A196, A197, A198 ; :: thesis: verum

end;

suppose A199: i >= j ; :: thesis: (Q * P) * (i,j) = (1. (K,n)) * (i,j)

then A200: i = j by A189, A196, XXREAL_0:1;
(1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i0)) . j0 by A186, A187, A189, A190, Th27
.= 1. K by A189, A190, A200, Th24 ;
hence (Q * P) * (i,j) = (1. (K,n)) * (i,j) by A183, A189, A196, A199, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence (Q * P) * (i,j) = (1. (K,n)) * (i,j) ; :: thesis: verum

end;

end;

end;

then A201: Q * P = 1. (K,n) by MATRIX_0:27;
A202: len Q = n by MATRIX_0:24;
A203: len (Base_FinSeq (K,n,1)) = n by Th23;
A204: len (a * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A205: for k being Nat st 1 <= k & k <= n holds
(Col (Q,1)) . k = (a * (Base_FinSeq (K,n,1))) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= n implies (Col (Q,1)) . k = (a * (Base_FinSeq (K,n,1))) . k )
assume that
A206: 1 <= k and
A207: k <= n ; :: thesis: (Col (Q,1)) . k = (a * (Base_FinSeq (K,n,1))) . k
A208: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A203, A206, A207, FINSEQ_4:15;
A209: k in dom (a * (Base_FinSeq (K,n,1))) by A204, A206, A207, FINSEQ_3:25;

A210: now :: thesis: ( k <> 1 implies (a * (Base_FinSeq (K,n,1))) . k = 0. K )

assume A211: k <> 1 ; :: thesis: (a * (Base_FinSeq (K,n,1))) . k = 0. K
thus (a * (Base_FinSeq (K,n,1))) . k = a * ((Base_FinSeq (K,n,1)) /. k) by A208, A209, FVSUM_1:50
.= a * (0. K) by A206, A207, A208, A211, Th25
.= 0. K ; :: thesis: verum

end;

A212: k in NAT by ORDINAL1:def 12;
k in Seg n by A206, A207, FINSEQ_1:1;
then A213: k in dom Q by A202, FINSEQ_1:def 3;

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

[k,1] in Indices Q by A8, A206, A207, MATRIX_0:31;
then A215: ex p being FinSequence of K st
( p = Q . k & Q * (k,1) = p . 1 ) by MATRIX_0:def 5;
assume A216: k <> 1 ; :: thesis: (Col (Q,1)) . k = 0. K
then 1 < k by A206, XXREAL_0:1;
then Q * (k,1) = (Base_FinSeq (K,n,k)) . 1 by A7, A207, A212, A215
.= 0. K by A8, A216, Th25 ;
hence (Col (Q,1)) . k = 0. K by A213, MATRIX_0:def 8; :: thesis: verum

end;

A217: now :: thesis: ( k = 1 implies (a * (Base_FinSeq (K,n,1))) . k = a )

assume A218: k = 1 ; :: thesis: (a * (Base_FinSeq (K,n,1))) . k = a
thus (a * (Base_FinSeq (K,n,1))) . k = a * ((Base_FinSeq (K,n,1)) /. k) by A208, A209, FVSUM_1:50
.= a * (1. K) by A207, A208, A218, Th24
.= a ; :: thesis: verum

end;

1 <= n by A206, A207, XXREAL_0:2;
then 1 in dom Q by A202, FINSEQ_3:25;
hence (Col (Q,1)) . k = (a * (Base_FinSeq (K,n,1))) . k by A5, A210, A217, A214, MATRIX_0:def 8; :: thesis: verum

end;

A219: 0 + 1 <= n by A1, NAT_1:13;
A220: len P = n by MATRIX_0:24;
then A221: 1 in Seg (len P) by A219, FINSEQ_1:1;
then A222: 1 in dom P by FINSEQ_1:def 3;
A223: width P = n by MATRIX_0:24;
then A224: len (Line (P,1)) = n by MATRIX_0:def 7;
then A225: 1 in dom (Line (P,1)) by A220, A221, FINSEQ_1:def 3;
A226: 1 in Seg (width P) by A223, A219, FINSEQ_1:1;
A227: for j being Element of NAT st 1 < j & j <= n holds
(P * Q) * (1,j) = 0. K

proof

let j be Element of NAT ; :: thesis: ( 1 < j & j <= n implies (P * Q) * (1,j) = 0. K )
assume that
A228: 1 < j and
A229: j <= n ; :: thesis: (P * Q) * (1,j) = 0. K
A230: len (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) = len ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) by Th6
.= len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
reconsider p = Col (Q,j), q = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) as FinSequence of K ;
A231: len (Base_FinSeq (K,n,j)) = n by Th23;
A232: len ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
A233: 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
A234: 1 <= k and
A235: k <= n ; :: thesis: p . k = q . k
A236: k in dom Q by A202, A234, A235, FINSEQ_3:25;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A237: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A234, A235, FINSEQ_4:15;
A238: ( k in dom ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) & (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k ) by A203, A232, A234, A235, FINSEQ_3:25, FINSEQ_4:15;
A239: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k = ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) . k by Th6
.= (- (a * (P * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A238, FVSUM_1:50 ;

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

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

(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A231, A234, A235, FINSEQ_4:15
.= 0. K by A228, A235, A240, Th25 ;
then q . k = ((- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k) + (0. K) by A230, A231, A234, A235, Th5;
then A241: q . k = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k by RLVECT_1:4;
A242: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- (a * (P * (1,j)))) * (1_ K) by A235, A239, A237, A240, Th24
.= - (a * (P * (1,j))) ;
p . k = Q * (1,j) by A236, A240, MATRIX_0:def 8
.= - (a * (P * (1,j))) by A6, A228, A229 ;
hence p . k = q . k by A230, A234, A235, A242, A241, FINSEQ_4:15; :: thesis: verum

end;

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

[k,j] in Indices Q by A228, A229, A234, A235, MATRIX_0:31;
then consider p2 being FinSequence of K such that
A244: p2 = Q . k and
A245: Q * (k,j) = p2 . j by MATRIX_0:def 5;
A246: k in NAT by ORDINAL1:def 12;
A247: p . k = p2 . j by A236, A245, MATRIX_0:def 8
.= (Base_FinSeq (K,n,k)) . j by A7, A235, A243, A244, A246 ;

now :: thesis: p . k = q . k

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

suppose A248: k <> j ; :: thesis: p . k = q . k

(- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- (a * (P * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A230, A234, A235, A239, FINSEQ_4:15
.= (- (a * (P * (1,j)))) * (0. K) by A235, A237, A243, Th25
.= 0. K ;
then q . k = (0. K) + ((Base_FinSeq (K,n,j)) /. k) by A230, A231, A234, A235, Th5
.= (Base_FinSeq (K,n,j)) /. k by RLVECT_1:4
.= (Base_FinSeq (K,n,j)) . k by A231, A234, A235, FINSEQ_4:15
.= 0. K by A234, A235, A248, Th25 ;
hence p . k = q . k by A228, A229, A247, A248, Th25; :: thesis: verum

end;

suppose A249: k = j ; :: thesis: p . k = q . k

(- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- (a * (P * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A230, A234, A235, A239, FINSEQ_4:15
.= (- (a * (P * (1,j)))) * (0. K) by A235, A237, A243, Th25
.= 0. K ;
then q . k = (0. K) + ((Base_FinSeq (K,n,j)) /. k) by A230, A231, A234, A235, Th5
.= (Base_FinSeq (K,n,j)) /. k by RLVECT_1:4
.= (Base_FinSeq (K,n,j)) . k by A231, A234, A235, FINSEQ_4:15
.= 1. K by A234, A235, A249, Th24 ;
hence p . k = q . k by A234, A235, A247, A249, Th24; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

A250: width P = n by MATRIX_0:24;
then A251: len (Line (P,1)) = n by MATRIX_0:def 7;
then A252: (Line (P,1)) /. 1 = (Line (P,1)) . 1 by A219, FINSEQ_4:15
.= a " by A3, A226, MATRIX_0:def 7 ;
A253: j in Seg n by A228, A229, FINSEQ_1:1;
A254: len (Col (Q,j)) = len Q by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
len ((- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j))) = n by A230, A231, Th2;
then A255: Col (Q,j) = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) by A254, A233, FINSEQ_1:14;
A256: (Line (P,1)) /. j = (Line (P,1)) . j by A228, A229, A251, FINSEQ_4:15
.= P * (1,j) by A253, A250, MATRIX_0:def 7 ;
[1,j] in Indices (P * Q) by A219, A228, A229, MATRIX_0:31;
then (P * Q) * (1,j) = |((Line (P,1)),(Col (Q,j)))| by A202, A250, MATRIX_3:def 4
.= |((Line (P,1)),(- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))))| + |((Line (P,1)),(Base_FinSeq (K,n,j)))| by A224, A230, A231, A255, Th11
.= |((Line (P,1)),((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))))| + |((Line (P,1)),(Base_FinSeq (K,n,j)))| by Th6
.= ((- (a * (P * (1,j)))) * |((Line (P,1)),(Base_FinSeq (K,n,1)))|) + |((Line (P,1)),(Base_FinSeq (K,n,j)))| by A224, A203, Th10
.= ((- (a * (P * (1,j)))) * (a ")) + |((Line (P,1)),(Base_FinSeq (K,n,j)))| by A224, A219, A252, Th35
.= (- ((a * (P * (1,j))) * (a "))) + |((Line (P,1)),(Base_FinSeq (K,n,j)))| by VECTSP_1:9
.= (- ((P * (1,j)) * (a * (a ")))) + |((Line (P,1)),(Base_FinSeq (K,n,j)))| by GROUP_1:def 3
.= (- ((P * (1,j)) * (1_ K))) + |((Line (P,1)),(Base_FinSeq (K,n,j)))| by A2, VECTSP_1:def 10
.= (- ((P * (1,j)) * (1. K))) + ((Line (P,1)) /. j) by A224, A228, A229, Th35
.= (- (P * (1,j))) + (P * (1,j)) by A256
.= 0. K by RLVECT_1:5 ;
hence (P * Q) * (1,j) = 0. K ; :: thesis: verum

end;

A257: Indices Q = [:(Seg n),(Seg n):] by MATRIX_0:24;
A258: for i, j being Element of NAT st 1 < i & i <= n & i = j holds
(P * Q) * (i,j) = 1. K

proof

let i, j be Element of NAT ; :: thesis: ( 1 < i & i <= n & i = j implies (P * Q) * (i,j) = 1. K )
assume that
A259: 1 < i and
A260: i <= n and
A261: i = j ; :: thesis: (P * Q) * (i,j) = 1. K
A262: len (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) = len ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) by Th6
.= len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
reconsider p = Col (Q,j), q = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) as FinSequence of K ;
A263: len (Base_FinSeq (K,n,j)) = n by Th23;
A264: j in Seg n by A259, A260, A261, FINSEQ_1:1;
A265: for k being Nat st 1 <= k & k <= n holds
p . k = q . k

proof

A266: len ((- (a * (P * (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
A267: 1 <= k and
A268: k <= n ; :: thesis: p . k = q . k
A269: k in Seg n by A267, A268, FINSEQ_1:1;
len ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
then A270: k in dom ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) by A267, A268, FINSEQ_3:25;
A271: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A203, A267, A268, FINSEQ_4:15;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A272: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A267, A268, FINSEQ_4:15;
k in dom Q by A202, A267, A268, FINSEQ_3:25;
then A273: p . k = Q * (k,j) by MATRIX_0:def 8;
A274: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k = ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) . k by Th6
.= (- (a * (P * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A270, A271, FVSUM_1:50 ;

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

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

k <= len (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) by A268, A266, Th6;
then A276: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- (a * (P * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A267, A274, FINSEQ_4:15
.= (- (a * (P * (1,j)))) * (1. K) by A219, A272, A275, Th24 ;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A263, A267, A268, FINSEQ_4:15
.= 0. K by A259, A261, A268, A275, Th25 ;
then q . k = ((- (a * (P * (1,j)))) * (1. K)) + (0. K) by A262, A263, A267, A268, A276, Th5
.= (- (a * (P * (1,j)))) * (1. K) by RLVECT_1:4
.= - (a * (P * (1,j))) ;
hence p . k = q . k by A6, A259, A260, A261, A273, A275; :: thesis: verum

end;

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

[k,j] in Indices Q by A257, A264, A269, ZFMISC_1:87;
then A278: ex p2 being FinSequence of K st
( p2 = Q . k & Q * (k,j) = p2 . j ) by MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then A279: p . k = (Base_FinSeq (K,n,k)) . j by A7, A268, A273, A277, A278;

now :: thesis: p . k = q . k

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

suppose A280: k <> j ; :: thesis: p . k = q . k

then A281: p . k = 0. K by A259, A260, A261, A279, Th25;
A282: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A262, A267, A268, FINSEQ_4:15;
A283: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- (a * (P * (1,j)))) * (0. K) by A268, A271, A274, A277, Th25
.= 0. K ;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A263, A267, A268, FINSEQ_4:15
.= 0. K by A267, A268, A280, Th25 ;
then q . k = (0. K) + (0. K) by A262, A263, A267, A268, A282, A283, Th5;
hence p . k = q . k by A281, RLVECT_1:4; :: thesis: verum

end;

suppose A284: k = j ; :: thesis: p . k = q . k

then A285: p . k = 1. K by A267, A268, A279, Th24;
A286: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A262, A267, A268, FINSEQ_4:15;
A287: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- (a * (P * (1,j)))) * (0. K) by A268, A271, A274, A277, Th25
.= 0. K ;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A263, A267, A268, FINSEQ_4:15
.= 1. K by A259, A260, A261, A284, Th24 ;
then q . k = (0. K) + (1. K) by A262, A263, A267, A268, A286, A287, Th5;
hence p . k = q . k by A285, RLVECT_1:4; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

[i,j] in Indices P by A259, A260, A261, MATRIX_0:31;
then consider p1 being FinSequence of K such that
A288: p1 = P . i and
A289: P * (i,j) = p1 . j by MATRIX_0:def 5;
p1 = Base_FinSeq (K,n,i) by A4, A259, A260, A288;
then A290: p1 . j = 1. K by A259, A260, A261, Th24;
A291: len (Col (Q,j)) = len Q by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
len ((- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j))) = n by A262, A263, Th2;
then A292: Col (Q,j) = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) by A291, A265, FINSEQ_1:14;
A293: width P = n by MATRIX_0:24;
then A294: len (Line (P,i)) = n by MATRIX_0:def 7;
then A295: (Line (P,i)) /. 1 = (Line (P,i)) . 1 by A219, FINSEQ_4:15
.= P * (i,1) by A226, MATRIX_0:def 7 ;
A296: (Line (P,i)) /. j = (Line (P,i)) . j by A259, A260, A261, A294, FINSEQ_4:15
.= P * (i,j) by A264, A293, MATRIX_0:def 7 ;
[i,j] in Indices (P * Q) by A259, A260, A261, MATRIX_0:31;
then A297: (P * Q) * (i,j) = |((Line (P,i)),(Col (Q,j)))| by A202, A293, MATRIX_3:def 4
.= |((Line (P,i)),(- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))))| + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by A262, A263, A292, A294, Th11
.= |((Line (P,i)),((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))))| + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by Th6
.= ((- (a * (P * (1,j)))) * |((Line (P,i)),(Base_FinSeq (K,n,1)))|) + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by A203, A294, Th10
.= ((- (a * (P * (1,j)))) * (P * (i,1))) + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by A219, A294, A295, Th35
.= (- ((a * (P * (1,j))) * (P * (i,1)))) + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by VECTSP_1:9
.= (- ((P * (1,j)) * (a * (P * (i,1))))) + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by GROUP_1:def 3
.= (- ((P * (1,j)) * (a * (P * (i,1))))) + (P * (i,j)) by A259, A260, A261, A294, A296, Th35 ;
A298: 1 <= n by A259, A260, XXREAL_0:2;
[i,1] in Indices P by A8, A259, A260, MATRIX_0:31;
then consider p2 being FinSequence of K such that
A299: p2 = P . i and
A300: P * (i,1) = p2 . 1 by MATRIX_0:def 5;
p2 = Base_FinSeq (K,n,i) by A4, A259, A260, A299;
hence (P * Q) * (i,j) = (- ((P * (1,j)) * (a * (0. K)))) + (P * (i,j)) by A259, A298, A297, A300, Th25
.= (- ((P * (1,j)) * (0. K))) + (P * (i,j))
.= (- (0. K)) + (P * (i,j))
.= (0. K) + (1. K) by A289, A290, RLVECT_1:12
.= 1. K by RLVECT_1:4 ;
:: thesis: verum

end;

len (Col (Q,1)) = len Q by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
then A301: Col (Q,1) = a * (Base_FinSeq (K,n,1)) by A204, A205, FINSEQ_1:14;
A302: Indices (P * Q) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A303: for i, j being Element of NAT st 1 < i & i <= n & 1 <= j & j <= n & i <> j holds
(P * Q) * (i,j) = 0. K

proof

A304: len (a * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
let i, j be Element of NAT ; :: thesis: ( 1 < i & i <= n & 1 <= j & j <= n & i <> j implies (P * Q) * (i,j) = 0. K )
assume that
A305: 1 < i and
A306: i <= n and
A307: 1 <= j and
A308: j <= n and
A309: i <> j ; :: thesis: (P * Q) * (i,j) = 0. K
A310: [i,j] in Indices (P * Q) by A305, A306, A307, A308, MATRIX_0:31;
A311: j in Seg n by A307, A308, FINSEQ_1:1;
A312: len (Col (Q,j)) = len Q by MATRIX_0:def 8
.= n by MATRIX_0:24 ;
A313: [i,1] in Indices P by A8, A305, A306, MATRIX_0:31;
A314: len (Base_FinSeq (K,n,j)) = n by Th23;
A315: len (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) = len ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) by Th6
.= len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
then A316: len ((- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j))) = n by A314, Th2;
A317: [i,j] in Indices P by A305, A306, A307, A308, MATRIX_0:31;

now :: thesis: (P * Q) * (i,j) = 0. K

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

suppose A318: j > 1 ; :: thesis: (P * Q) * (i,j) = 0. K

reconsider p = Col (Q,j), q = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) as FinSequence of K ;
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
A319: 1 <= k and
A320: k <= n ; :: thesis: p . k = q . k
A321: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A203, A319, A320, FINSEQ_4:15;
A322: len ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) = len (Base_FinSeq (K,n,1)) by MATRIXR1:16
.= n by Th23 ;
then A323: k in dom ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) by A319, A320, FINSEQ_3:25;
A324: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k = ((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))) . k by Th6
.= (- (a * (P * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A323, A321, FVSUM_1:50 ;
len (Base_FinSeq (K,n,1)) = n by Th23;
then A325: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A319, A320, FINSEQ_4:15;
k in dom Q by A202, A319, A320, FINSEQ_3:25;
then A326: p . k = Q * (k,j) by MATRIX_0:def 8;

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

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

k <= len (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) by A320, A322, Th6;
then A328: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- (a * (P * (1,j)))) * ((Base_FinSeq (K,n,1)) /. k) by A319, A324, FINSEQ_4:15
.= (- (a * (P * (1,j)))) * (1. K) by A219, A325, A327, Th24 ;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A314, A319, A320, FINSEQ_4:15
.= 0. K by A318, A320, A327, Th25 ;
then q . k = ((- (a * (P * (1,j)))) * (1. K)) + (0. K) by A315, A314, A319, A320, A328, Th5
.= (- (a * (P * (1,j)))) * (1_ K) by RLVECT_1:4
.= - (a * (P * (1,j))) ;
hence p . k = q . k by A6, A308, A318, A326, A327; :: thesis: verum

end;

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

[k,j] in Indices Q by A307, A308, A319, A320, MATRIX_0:31;
then A330: ex p2 being FinSequence of K st
( p2 = Q . k & Q * (k,j) = p2 . j ) by MATRIX_0:def 5;
k in NAT by ORDINAL1:def 12;
then A331: p . k = (Base_FinSeq (K,n,k)) . j by A7, A320, A326, A329, A330;
A332: k <= len (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) by A320, A322, Th6;

now :: thesis: p . k = q . k

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

suppose A333: k <> j ; :: thesis: p . k = q . k

(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A314, A319, A320, FINSEQ_4:15
.= 0. K by A319, A320, A333, Th25 ;
then q . k = ((- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k) + (0. K) by A315, A314, A319, A320, Th5;
then A334: q . k = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k by RLVECT_1:4
.= (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A319, A332, FINSEQ_4:15 ;
(- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- (a * (P * (1,j)))) * (0. K) by A320, A324, A325, A329, Th25
.= 0. K ;
hence p . k = q . k by A307, A308, A331, A333, A334, Th25; :: thesis: verum

end;

suppose A335: k = j ; :: thesis: p . k = q . k

then A336: p . k = 1. K by A319, A320, A331, Th24;
A337: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) /. k = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k by A315, A319, A320, FINSEQ_4:15;
A338: (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) . k = (- (a * (P * (1,j)))) * (0. K) by A320, A321, A324, A329, Th25
.= 0. K ;
(Base_FinSeq (K,n,j)) /. k = (Base_FinSeq (K,n,j)) . k by A314, A319, A320, FINSEQ_4:15
.= 1. K by A319, A320, A335, Th24 ;
then q . k = (0. K) + (1. K) by A315, A314, A319, A320, A337, A338, Th5;
hence p . k = q . k by A336, RLVECT_1:4; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

then A339: Col (Q,j) = (- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))) + (Base_FinSeq (K,n,j)) by A312, A316, FINSEQ_1:14;
A340: 1 <= n by A305, A306, XXREAL_0:2;
A341: width P = n by MATRIX_0:24;
then A342: len (Line (P,i)) = n by MATRIX_0:def 7;
then A343: (Line (P,i)) /. j = (Line (P,i)) . j by A307, A308, FINSEQ_4:15
.= P * (i,j) by A311, A341, MATRIX_0:def 7 ;
A344: (Line (P,i)) /. 1 = (Line (P,i)) . 1 by A219, A342, FINSEQ_4:15
.= P * (i,1) by A226, MATRIX_0:def 7 ;
A345: (P * Q) * (i,j) = |((Line (P,i)),(Col (Q,j)))| by A202, A310, A341, MATRIX_3:def 4
.= |((Line (P,i)),(- ((a * (P * (1,j))) * (Base_FinSeq (K,n,1)))))| + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by A315, A314, A339, A342, Th11
.= |((Line (P,i)),((- (a * (P * (1,j)))) * (Base_FinSeq (K,n,1))))| + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by Th6
.= ((- (a * (P * (1,j)))) * |((Line (P,i)),(Base_FinSeq (K,n,1)))|) + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by A203, A342, Th10
.= ((- (a * (P * (1,j)))) * (P * (i,1))) + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by A219, A342, A344, Th35
.= (- ((a * (P * (1,j))) * (P * (i,1)))) + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by VECTSP_1:9
.= (- ((P * (1,j)) * (a * (P * (i,1))))) + |((Line (P,i)),(Base_FinSeq (K,n,j)))| by GROUP_1:def 3
.= (- ((P * (1,j)) * (a * (P * (i,1))))) + (P * (i,j)) by A307, A308, A342, A343, Th35 ;
consider p2 being FinSequence of K such that
A346: p2 = P . i and
A347: P * (i,1) = p2 . 1 by A313, MATRIX_0:def 5;
consider p1 being FinSequence of K such that
A348: p1 = P . i and
A349: P * (i,j) = p1 . j by A317, MATRIX_0:def 5;
p1 = Base_FinSeq (K,n,i) by A4, A305, A306, A348;
then A350: p1 . j = 0. K by A307, A308, A309, Th25;
p2 = Base_FinSeq (K,n,i) by A4, A305, A306, A346;
then (P * Q) * (i,j) = (- ((P * (1,j)) * (a * (0. K)))) + (P * (i,j)) by A305, A340, A345, A347, Th25
.= (- ((P * (1,j)) * (0. K))) + (P * (i,j))
.= (- (0. K)) + (P * (i,j))
.= (0. K) + (0. K) by A349, A350, RLVECT_1:12
.= 0. K by RLVECT_1:4 ;
hence (P * Q) * (i,j) = 0. K ; :: thesis: verum

end;

suppose A351: j <= 1 ; :: thesis: (P * Q) * (i,j) = 0. K

reconsider p = Col (Q,j), q = a * (Base_FinSeq (K,n,1)) as FinSequence of K ;
A352: 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
A353: 1 <= k and
A354: k <= n ; :: thesis: p . k = q . k
A355: k in dom Q by A202, A353, A354, FINSEQ_3:25;
A356: len (Base_FinSeq (K,n,1)) = n by Th23;
then A357: (Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A353, A354, FINSEQ_4:15;
k in dom (a * (Base_FinSeq (K,n,1))) by A204, A353, A354, FINSEQ_3:25;
then A358: (a * (Base_FinSeq (K,n,1))) . k = a * ((Base_FinSeq (K,n,1)) /. k) by A357, FVSUM_1:50;

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

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

then A360: q . k = a * (1. K) by A354, A357, A358, Th24
.= a ;
p . k = Q * (1,j) by A355, A359, MATRIX_0:def 8
.= a by A5, A307, A351, XXREAL_0:1 ;
hence p . k = q . k by A360; :: thesis: verum

end;

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

[k,j] in Indices Q by A307, A308, A353, A354, MATRIX_0:31;
then A362: ex p2 being FinSequence of K st
( p2 = Q . k & Q * (k,j) = p2 . j ) by MATRIX_0:def 5;
A363: k in NAT by ORDINAL1:def 12;
A364: p . k = Q * (k,j) by A355, MATRIX_0:def 8
.= (Base_FinSeq (K,n,k)) . j by A7, A354, A361, A362, A363 ;

now :: thesis: p . k = q . k

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

suppose A365: k <> j ; :: thesis: p . k = q . k

(Base_FinSeq (K,n,1)) /. k = (Base_FinSeq (K,n,1)) . k by A353, A354, A356, FINSEQ_4:15;
then a * ((Base_FinSeq (K,n,1)) /. k) = a * (0. K) by A354, A361, Th25
.= 0. K ;
hence p . k = q . k by A307, A308, A358, A364, A365, Th25; :: thesis: verum

end;

suppose k = j ; :: thesis: p . k = q . k

hence p . k = q . k by A351, A361; :: thesis: verum

end;

end;

end;

hence p . k = q . k ; :: thesis: verum

end;

end;

end;

A366: 1 <= n by A305, A306, XXREAL_0:2;
A367: len (Line (P,i)) = n by A223, MATRIX_0:def 7;
then A368: (Line (P,i)) /. 1 = (Line (P,i)) . 1 by A219, FINSEQ_4:15
.= P * (i,1) by A226, MATRIX_0:def 7 ;
A369: (P * Q) * (i,j) = |((Line (P,i)),(Col (Q,j)))| by A202, A223, A310, MATRIX_3:def 4
.= |((Line (P,i)),(a * (Base_FinSeq (K,n,1))))| by A312, A304, A352, FINSEQ_1:14
.= a * |((Line (P,i)),(Base_FinSeq (K,n,1)))| by A203, A367, Th10
.= a * (P * (i,1)) by A219, A367, A368, Th35 ;
consider p2 being FinSequence of K such that
A370: p2 = P . i and
A371: P * (i,1) = p2 . 1 by A313, MATRIX_0:def 5;
p2 = Base_FinSeq (K,n,i) by A4, A305, A306, A370;
hence (P * Q) * (i,j) = a * (0. K) by A305, A366, A369, A371, Th25
.= 0. K ;
:: thesis: verum

end;

end;

end;

hence (P * Q) * (i,j) = 0. K ; :: thesis: verum

end;

A372: len (a * (Line (P,1))) = len (Line (P,1)) by MATRIXR1:16
.= n by A223, MATRIX_0:def 7 ;
( Indices P = [:(Seg n),(Seg n):] & [1,1] in Indices P ) by A219, MATRIX_0:24, MATRIX_0:31;
then A373: (P * Q) * (1,1) = |((Line (P,1)),(Col (Q,1)))| by A202, A223, A302, MATRIX_3:def 4
.= a * |((Line (P,1)),(Base_FinSeq (K,n,1)))| by A224, A203, A301, Th10
.= a * ((Line (P,1)) /. 1) by A224, A219, Th35
.= (a * (Line (P,1))) /. 1 by A225, POLYNOM1:def 1
.= (a * (Line (P,1))) . 1 by A219, A372, FINSEQ_4:15
.= a * (P * (1,1)) by A226, A222, MATRIX12:3
.= 1. K by A2, A3, VECTSP_1:def 10 ;
for i, j being Nat st [i,j] in Indices (P * Q) holds
(P * Q) * (i,j) = (1. (K,n)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (P * Q) implies (P * Q) * (i,j) = (1. (K,n)) * (i,j) )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;
assume A374: [i,j] in Indices (P * Q) ; :: thesis: (P * Q) * (i,j) = (1. (K,n)) * (i,j)
then A375: i in Seg n by A302, ZFMISC_1:87;
then A376: 1 <= i by FINSEQ_1:1;
A377: i <= n by A375, FINSEQ_1:1;
A378: j in Seg n by A302, A374, ZFMISC_1:87;
then A379: 1 <= j by FINSEQ_1:1;
A380: j <= n by A378, FINSEQ_1:1;

per cases ( 1 < i or 1 = i ) by A376, XXREAL_0:1;

suppose A381: 1 < i ; :: thesis: (P * Q) * (i,j) = (1. (K,n)) * (i,j)

now :: thesis: (P * Q) * (i,j) = (1. (K,n)) * (i,j)

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

suppose A382: i <> j ; :: thesis: (P * Q) * (i,j) = (1. (K,n)) * (i,j)

A383: (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i0)) . j0 by A376, A377, A379, A380, Th27
.= 0. K by A379, A380, A382, Th25 ;
thus (P * Q) * (i,j) = (P * Q) * (i0,j0)
.= (1. (K,n)) * (i,j) by A303, A377, A379, A380, A381, A382, A383 ; :: thesis: verum

end;

suppose A384: i = j ; :: thesis: (P * Q) * (i,j) = (1. (K,n)) * (i,j)

A385: (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i0)) . j0 by A376, A377, A379, A380, Th27
.= 1. K by A379, A380, A384, Th24 ;
thus (P * Q) * (i,j) = (P * Q) * (i0,j0)
.= (1. (K,n)) * (i,j) by A258, A380, A381, A384, A385 ; :: thesis: verum

end;

end;

end;

hence (P * Q) * (i,j) = (1. (K,n)) * (i,j) ; :: thesis: verum

end;

suppose A386: 1 = i ; :: thesis: (P * Q) * (i,j) = (1. (K,n)) * (i,j)

now :: thesis: (P * Q) * (i,j) = (1. (K,n)) * (i,j)

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

suppose A387: i < j ; :: thesis: (P * Q) * (i,j) = (1. (K,n)) * (i,j)

A388: (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i0)) . j0 by A376, A377, A379, A380, Th27
.= 0. K by A379, A380, A387, Th25 ;
thus (P * Q) * (i,j) = (P * Q) * (i0,j0)
.= (1. (K,n)) * (i,j) by A227, A380, A386, A387, A388 ; :: thesis: verum

end;

suppose A389: i >= j ; :: thesis: (P * Q) * (i,j) = (1. (K,n)) * (i,j)

then A390: i = j by A379, A386, XXREAL_0:1;
(1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i0)) . j0 by A376, A377, A379, A380, Th27
.= 1. K by A379, A380, A390, Th24 ;
hence (P * Q) * (i,j) = (1. (K,n)) * (i,j) by A373, A379, A386, A389, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence (P * Q) * (i,j) = (1. (K,n)) * (i,j) ; :: thesis: verum

end;

end;

end;

then A391: P * Q = 1. (K,n) by MATRIX_0:27;
hence P is invertible by A201, Th19; :: thesis: Q = P ~
thus Q = P ~ by A391, A201, Th18; :: thesis: verum