let n be Element of NAT ; :: thesis:
let K be Field; :: thesis:
let A, B be Matrix of n,K; :: thesis:
thus ( B * A = 1. K,n implies ex B2 being Matrix of n,K st A * B2 = 1. K,n ) :: thesis:

defpred S₁[ Element of NAT ] means for D, B3 being Matrix of $1,K st B3 * D = 1. K,$1 holds
ex B4 being Matrix of $1,K st D * B4 = 1. K,$1;
assume A1: B * A = 1. K,n ; :: thesis:
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
assume A3: S₁[k] ; :: thesis:
for A2, B3 being Matrix of k + 1,K st B3 * A2 = 1. K,(k + 1) holds
ex B4 being Matrix of k + 1,K st A2 * B4 = 1. K,(k + 1)

proof

let A2, B2 be Matrix of k + 1,K; :: thesis:
A4: Indices (1. K,(k + 1)) = [:(Seg (k + 1)),(Seg (k + 1)):] by MATRIX_1:25;
assume A5: B2 * A2 = 1. K,(k + 1) ; :: thesis:
then A6: (Det B2) * (Det A2) = Det (1. K,(k + 1)) by MATRIXR2:45;

now

assume A2 = 0. K,(k + 1) ; :: thesis:
then A2 = 0. K,(k + 1),(k + 1) by MATRIX_3:def 1;
then Det A2 = 0. K by MATRIX_7:15, NAT_1:12;
then A7: (Det B2) * (Det A2) = 0. K by VECTSP_1:36;
not 0. K = 1_ K ;
hence contradiction by A6, A7, MATRIX_7:16, NAT_1:12; :: thesis:

end;

then consider B, C being Matrix of k + 1,K such that
A8: B is invertible and
A9: C is invertible and
A10: ((B * A2) * C) * 1,1 = 1. K and
A11: for i being Element of NAT st 1 < i & i <= k + 1 holds
((B * A2) * C) * i,1 = 0. K and
A12: for j being Element of NAT st 1 < j & j <= k + 1 holds
((B * A2) * C) * 1,j = 0. K by Th53;
set A3 = (B * A2) * C;
set B3 = ((C ~ ) * B2) * (B ~ );
A13: width (((C ~ ) * B2) * (B ~ )) = k + 1 by MATRIX_1:25;
A14: width ((B * A2) * C) = k + 1 by MATRIX_1:25;
A15: for j being Nat st 1 <= j & j <= len (Line ((B * A2) * C),1) holds
(Line ((B * A2) * C),1) . j = (Base_FinSeq K,(k + 1),1) . j

proof

let j be Nat; :: thesis:
assume that
A16: 1 <= j and
A17: j <= len (Line ((B * A2) * C),1) ; :: thesis:
A18: j <= k + 1 by A14, A17, MATRIX_1:def 8;
len (Line ((B * A2) * C),1) = width ((B * A2) * C) by MATRIX_1:def 8;
then A19: j in Seg (width ((B * A2) * C)) by A16, A17, FINSEQ_1:3;

per cases by A16, XXREAL_0:1;

suppose A20: 1 = j ; :: thesis:

then (Line ((B * A2) * C),1) . j = 1. K by A10, A19, MATRIX_1:def 8;
hence (Line ((B * A2) * C),1) . j = (Base_FinSeq K,(k + 1),1) . j by A18, A20, Th24; :: thesis:

end;

suppose A21: 1 < j ; :: thesis:

A22: j in NAT by ORDINAL1:def 13;
(Line ((B * A2) * C),1) . j = ((B * A2) * C) * 1,j by A19, MATRIX_1:def 8
.= 0. K by A12, A18, A21, A22 ;
hence (Line ((B * A2) * C),1) . j = (Base_FinSeq K,(k + 1),1) . j by A18, A21, Th25; :: thesis:

end;

A23: len <*(0. K)*> = 1 by FINSEQ_1:57;
deffunc H₁( Nat, Nat) -> Element of the carrier of K = ((B * A2) * C) * ($1 + 1),($2 + 1);
A24: len (A2 * C) = k + 1 by MATRIX_1:25;
consider F being Matrix of k,k,K such that
A25: for i, j being Nat st [i,j] in Indices F holds
F * i,j = H₁(i,j) from MATRIX_1:sch 1();
A26: len F = k by MATRIX_1:25;
deffunc H₂( Nat, Nat) -> Element of the carrier of K = (((C ~ ) * B2) * (B ~ )) * ($1 + 1),($2 + 1);
A27: len C = k + 1 by MATRIX_1:25;
consider G being Matrix of k,k,K such that
A28: for i, j being Nat st [i,j] in Indices G holds
G * i,j = H₂(i,j) from MATRIX_1:sch 1();
A29: len ((B * A2) * C) = k + 1 by MATRIX_1:25;
A30: (((C ~ ) * B2) * (B ~ )) * ((B * A2) * C) = (((C ~ ) * B2) * (B ~ )) * (B * (A2 * C)) by Th17
.= ((((Inv C) * B2) * (Inv B)) * B) * (A2 * C) by Th17
.= (((Inv C) * B2) * ((Inv B) * B)) * (A2 * C) by Th17
.= (((Inv C) * B2) * (1. K,(k + 1))) * (A2 * C) by A8, Th18
.= ((Inv C) * B2) * ((1. K,(k + 1)) * (A2 * C)) by Th17
.= ((Inv C) * B2) * (A2 * C) by A24, MATRIXR2:68
.= (((Inv C) * B2) * A2) * C by Th17
.= ((Inv C) * (1. K,(k + 1))) * C by A5, Th17
.= (Inv C) * ((1. K,(k + 1)) * C) by Th17
.= (Inv C) * C by A27, MATRIXR2:68
.= 1. K,(k + 1) by A9, Th18 ;
A31: for i being Nat st 1 < i & i <= k + 1 holds
(((C ~ ) * B2) * (B ~ )) * i,1 = (1. K,(k + 1)) * i,1

proof

A32: len (Base_FinSeq K,(k + 1),1) = k + 1 by Th23;
let i be Nat; :: thesis:
A33: len (Col ((B * A2) * C),1) = len ((B * A2) * C) by MATRIX_1:def 9
.= k + 1 by MATRIX_1:25 ;
A34: len ((B * A2) * C) = k + 1 by MATRIX_1:25;
A35: for k2 being Nat st 1 <= k2 & k2 <= len (Col ((B * A2) * C),1) holds
(Col ((B * A2) * C),1) . k2 = (Base_FinSeq K,(k + 1),1) . k2

proof

let k2 be Nat; :: thesis:
assume that
A36: 1 <= k2 and
A37: k2 <= len (Col ((B * A2) * C),1) ; :: thesis:
A38: k2 in NAT by ORDINAL1:def 13;

A39: now

per cases by A36, XXREAL_0:1;

suppose k2 = 1 ; :: thesis:

hence ((B * A2) * C) * k2,1 = (Base_FinSeq K,(k + 1),1) . k2 by A10, A33, A37, Th24; :: thesis:

end;

suppose A40: 1 < k2 ; :: thesis:

hence ((B * A2) * C) * k2,1 = 0. K by A11, A33, A38, A37
.= (Base_FinSeq K,(k + 1),1) . k2 by A33, A37, A40, Th25 ;
:: thesis:

end;

k2 in Seg (len ((B * A2) * C)) by A34, A33, A36, A37, FINSEQ_1:3;
then k2 in dom ((B * A2) * C) by FINSEQ_1:def 3;
hence (Col ((B * A2) * C),1) . k2 = (Base_FinSeq K,(k + 1),1) . k2 by A39, MATRIX_1:def 9; :: thesis:

end;

A41: len (Line (((C ~ ) * B2) * (B ~ )),i) = width (((C ~ ) * B2) * (B ~ )) by MATRIX_1:def 8
.= k + 1 by MATRIX_1:25 ;
assume A42: ( 1 < i & i <= k + 1 ) ; :: thesis:
then A43: 1 <= k + 1 by XXREAL_0:2;
A44: width (((C ~ ) * B2) * (B ~ )) = k + 1 by MATRIX_1:25;
then A45: 1 in Seg (width (((C ~ ) * B2) * (B ~ ))) by A43, FINSEQ_1:3;
[i,1] in Indices ((((C ~ ) * B2) * (B ~ )) * ((B * A2) * C)) by A42, A43, MATRIX_1:38;
then ((((C ~ ) * B2) * (B ~ )) * ((B * A2) * C)) * i,1 = |((Line (((C ~ ) * B2) * (B ~ )),i),(Col ((B * A2) * C),1))| by A44, A34, MATRIX_3:def 4
.= |((Line (((C ~ ) * B2) * (B ~ )),i),(Base_FinSeq K,(k + 1),1))| by A33, A32, A35, FINSEQ_1:18
.= (Line (((C ~ ) * B2) * (B ~ )),i) . 1 by A43, A41, Th35
.= (((C ~ ) * B2) * (B ~ )) * i,1 by A45, MATRIX_1:def 8 ;
hence (((C ~ ) * B2) * (B ~ )) * i,1 = (1. K,(k + 1)) * i,1 by A30; :: thesis:

end;

for i, j being Element of NAT st 1 <= i & i <= k & 1 <= j & j <= k holds
(G * F) * i,j = IFEQ i,j,(1. K),(0. K)

proof

let i, j be Element of NAT ; :: thesis:
assume that
A46: 1 <= i and
A47: i <= k and
A48: 1 <= j and
A49: j <= k ; :: thesis:
A50: [i,j] in Indices (G * F) by A46, A47, A48, A49, MATRIX_1:38;
A51: for k2 being Nat st k2 in dom <*(0. K)*> holds
(Col ((B * A2) * C),(j + 1)) . k2 = <*(0. K)*> . k2

proof

( j + 1 <= k + 1 & 1 < j + 1 ) by A48, A49, NAT_1:13, XREAL_1:9;
then A52: ((B * A2) * C) * 1,(j + 1) = 0. K by A12;
let k2 be Nat; :: thesis:
assume k2 in dom <*(0. K)*> ; :: thesis:
then k2 in Seg (len <*(0. K)*>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:4, FINSEQ_1:57;
then A53: k2 = 1 by TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then k2 in Seg (len ((B * A2) * C)) by A29, A53, FINSEQ_1:3;
then k2 in dom ((B * A2) * C) by FINSEQ_1:def 3;
then (Col ((B * A2) * C),(j + 1)) . k2 = 0. K by A53, A52, MATRIX_1:def 9;
hence (Col ((B * A2) * C),(j + 1)) . k2 = <*(0. K)*> . k2 by A53, FINSEQ_1:57; :: thesis:

end;

A54: len (Col F,j) = len F by MATRIX_1:def 9
.= k by MATRIX_1:25 ;
A55: i + 1 <= k + 1 by A47, XREAL_1:9;
A56: for k2 being Nat st k2 in dom <*(0. K)*> holds
(Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . k2 = <*(0. K)*> . k2

proof

let k2 be Nat; :: thesis:
A57: 1 < i + 1 by A46, NAT_1:13;
1 <= 1 + k by NAT_1:11;
then A58: [(i + 1),1] in Indices (1. K,(k + 1)) by A55, A57, MATRIX_1:38;
A59: (((C ~ ) * B2) * (B ~ )) * (i + 1),1 = (1. K,(k + 1)) * (i + 1),1 by A31, A55, A57
.= 0. K by A57, A58, MATRIX_1:def 12 ;
assume k2 in dom <*(0. K)*> ; :: thesis:
then k2 in Seg (len <*(0. K)*>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:4, FINSEQ_1:57;
then A60: k2 = 1 by TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then k2 in Seg (width (((C ~ ) * B2) * (B ~ ))) by A13, A60, FINSEQ_1:3;
then (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . k2 = 0. K by A60, A59, MATRIX_1:def 8;
hence (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . k2 = <*(0. K)*> . k2 by A60, FINSEQ_1:57; :: thesis:

end;

A61: for k2 being Nat st k2 in dom (Col F,j) holds
(Col ((B * A2) * C),(j + 1)) . ((len <*(0. K)*>) + k2) = (Col F,j) . k2

proof

reconsider j0 = j + 1 as Element of NAT ;
let k2 be Nat; :: thesis:
A62: len (Col F,(j0 -' 1)) = len F by MATRIX_1:def 9;
A63: j0 -' 1 = j by NAT_D:34;
assume A64: k2 in dom (Col F,j) ; :: thesis:
then A65: k2 in Seg (len (Col F,(j0 -' 1))) by A63, FINSEQ_1:def 3;
then A66: k2 <= k by A26, A62, FINSEQ_1:3;
then ( 1 <= k2 + 1 & k2 + 1 <= k + 1 ) by NAT_1:11, XREAL_1:9;
then A67: k2 + 1 in dom ((B * A2) * C) by A29, FINSEQ_3:27;
1 <= k2 by A65, FINSEQ_1:3;
then [k2,j] in Indices F by A48, A49, A66, MATRIX_1:38;
then [k2,(j0 -' 1)] in Indices F by NAT_D:34;
then A68: ((B * A2) * C) * (k2 + 1),((j0 -' 1) + 1) = F * k2,(j0 -' 1) by A25;
k2 in Seg k by A26, A64, A62, A63, FINSEQ_1:def 3;
then k2 in dom F by A26, FINSEQ_1:def 3;
then ((B * A2) * C) * (k2 + 1),((j0 -' 1) + 1) = (Col F,(j0 -' 1)) . k2 by A68, MATRIX_1:def 9;
hence (Col ((B * A2) * C),(j + 1)) . ((len <*(0. K)*>) + k2) = (Col F,j) . k2 by A23, A63, A67, MATRIX_1:def 9; :: thesis:

end;

A69: len (Line G,i) = width G by MATRIX_1:def 8
.= k by MATRIX_1:25 ;
A70: k + 1 = (len <*(0. K)*>) + k by FINSEQ_1:56;
A71: for k2 being Nat st k2 in dom (Line G,i) holds
(Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . ((len <*(0. K)*>) + k2) = (Line G,i) . k2

proof

let k2 be Nat; :: thesis:
A72: ( width (((C ~ ) * B2) * (B ~ )) = k + 1 & 1 <= k2 + 1 ) by MATRIX_1:25, NAT_1:11;
assume A73: k2 in dom (Line G,i) ; :: thesis:
then A74: k2 in Seg (len (Line G,i)) by FINSEQ_1:def 3;
A75: len (Line G,i) = width G by MATRIX_1:def 8
.= k by MATRIX_1:25 ;
then A76: k2 <= k by A74, FINSEQ_1:3;
1 <= k2 by A74, FINSEQ_1:3;
then [i,k2] in Indices G by A46, A47, A76, MATRIX_1:38;
then A77: (((C ~ ) * B2) * (B ~ )) * (i + 1),(k2 + 1) = G * i,k2 by A28;
k2 in Seg k by A73, A75, FINSEQ_1:def 3;
then k2 in Seg (width G) by MATRIX_1:25;
then A78: (((C ~ ) * B2) * (B ~ )) * (i + 1),(k2 + 1) = (Line G,i) . k2 by A77, MATRIX_1:def 8;
k2 + 1 <= k + 1 by A76, XREAL_1:9;
then k2 + 1 in Seg (width (((C ~ ) * B2) * (B ~ ))) by A72, FINSEQ_1:3;
then (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . (k2 + 1) = (Line G,i) . k2 by A78, MATRIX_1:def 8;
hence (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . ((len <*(0. K)*>) + k2) = (Line G,i) . k2 by FINSEQ_1:57; :: thesis:

end;

A79: width G = k by MATRIX_1:25;
( len (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) = width (((C ~ ) * B2) * (B ~ )) & len (Line G,i) = width G ) by MATRIX_1:def 8;
then dom (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) = Seg ((len <*(0. K)*>) + (len (Line G,i))) by A13, A79, A70, FINSEQ_1:def 3;
then A80: <*(0. K)*> ^ (Line G,i) = Line (((C ~ ) * B2) * (B ~ )),(i + 1) by A56, A71, FINSEQ_1:def 7;
A81: ( 1 <= i + 1 & 1 <= j + 1 ) by NAT_1:11;
A82: j + 1 <= k + 1 by A49, XREAL_1:9;

A83: now

per cases ;

suppose A84: i = j ; :: thesis:

[(i + 1),(j + 1)] in Indices (1. K,(k + 1)) by A81, A55, A82, MATRIX_1:38;
then (1. K,(k + 1)) * (i + 1),(j + 1) = 1. K by A84, MATRIX_1:def 12;
hence (1. K,(k + 1)) * (i + 1),(j + 1) = IFEQ i,j,(1. K),(0. K) by A84, FUNCOP_1:def 8; :: thesis:

end;

suppose A85: i <> j ; :: thesis:

[(i + 1),(j + 1)] in Indices (1. K,(k + 1)) by A81, A55, A82, MATRIX_1:38;
then ( i + 1 <> j + 1 implies (1. K,(k + 1)) * (i + 1),(j + 1) = 0. K ) by MATRIX_1:def 12;
hence (1. K,(k + 1)) * (i + 1),(j + 1) = IFEQ i,j,(1. K),(0. K) by A85, FUNCOP_1:def 8; :: thesis:

end;

( len (Col ((B * A2) * C),(j + 1)) = len ((B * A2) * C) & len (Col F,j) = len F ) by MATRIX_1:def 9;
then dom (Col ((B * A2) * C),(j + 1)) = Seg ((len <*(0. K)*>) + (len (Col F,j))) by A29, A26, A70, FINSEQ_1:def 3;
then A86: <*(0. K)*> ^ (Col F,j) = Col ((B * A2) * C),(j + 1) by A51, A61, FINSEQ_1:def 7;
[(i + 1),(j + 1)] in Indices ((((C ~ ) * B2) * (B ~ )) * ((B * A2) * C)) by A81, A55, A82, MATRIX_1:38;
then ((((C ~ ) * B2) * (B ~ )) * ((B * A2) * C)) * (i + 1),(j + 1) = |((Line (((C ~ ) * B2) * (B ~ )),(i + 1)),(Col ((B * A2) * C),(j + 1)))| by A13, A29, MATRIX_3:def 4
.= |(<*(0. K)*>,<*(0. K)*>)| + |((Line G,i),(Col F,j))| by A23, A80, A86, A69, A54, Th12
.= (0. K) + |((Line G,i),(Col F,j))| by Th22
.= |((Line G,i),(Col F,j))| by RLVECT_1:10 ;
hence (G * F) * i,j = IFEQ i,j,(1. K),(0. K) by A30, A26, A50, A79, A83, MATRIX_3:def 4; :: thesis:

end;

then G * F = 1. K,k by Th29;
then consider G2 being Matrix of k,K such that
A87: F * G2 = 1. K,k by A3;
deffunc H₃( Nat, Nat) -> Element of the carrier of K = IFEQ $1,1,(IFEQ $2,1,(1. K),(0. K)),(IFEQ $2,1,(0. K),(G2 * ($1 -' 1),($2 -' 1)));
A88: len G2 = k by MATRIX_1:25;
consider B4 being Matrix of k + 1,k + 1,K such that
A89: for i, j being Nat st [i,j] in Indices B4 holds
B4 * i,j = H₃(i,j) from MATRIX_1:sch 1();
A90: len B4 = k + 1 by MATRIX_1:25;
A91: width B4 = k + 1 by MATRIX_1:25;
A92: for j being Nat st 1 <= j & j <= len (Col B4,1) holds
(Col B4,1) . j = (Base_FinSeq K,(k + 1),1) . j

proof

let j be Nat; :: thesis:
assume that
A93: 1 <= j and
A94: j <= len (Col B4,1) ; :: thesis:
A95: j <= k + 1 by A90, A94, MATRIX_1:def 9;
then 1 <= k + 1 by A93, XXREAL_0:2;
then A96: [j,1] in Indices B4 by A93, A95, MATRIX_1:38;
len (Col B4,1) = len B4 by MATRIX_1:def 9;
then j in Seg (width B4) by A90, A91, A93, A94, FINSEQ_1:3;
then A97: j in dom B4 by A90, A91, FINSEQ_1:def 3;

per cases by A93, XXREAL_0:1;

suppose A98: 1 = j ; :: thesis:

(Col B4,1) . j = B4 * j,1 by A97, MATRIX_1:def 9
.= IFEQ j,1,(IFEQ 1,1,(1. K),(0. K)),(IFEQ 1,1,(0. K),(G2 * (j -' 1),(1 -' 1))) by A89, A96
.= IFEQ 1,1,(1. K),(0. K) by A98, FUNCOP_1:def 8
.= 1. K by FUNCOP_1:def 8 ;
hence (Col B4,1) . j = (Base_FinSeq K,(k + 1),1) . j by A95, A98, Th24; :: thesis:

end;

suppose A99: 1 < j ; :: thesis:

(Col B4,1) . j = B4 * j,1 by A97, MATRIX_1:def 9
.= IFEQ j,1,(IFEQ 1,1,(1. K),(0. K)),(IFEQ 1,1,(0. K),(G2 * (j -' 1),(1 -' 1))) by A89, A96
.= IFEQ 1,1,(0. K),(G2 * (j -' 1),(1 -' 1)) by A99, FUNCOP_1:def 8
.= 0. K by FUNCOP_1:def 8 ;
hence (Col B4,1) . j = (Base_FinSeq K,(k + 1),1) . j by A95, A99, Th25; :: thesis:

end;

A100: width (((B * A2) * C) * B4) = k + 1 by MATRIX_1:25;
A101: Indices (((B * A2) * C) * B4) = [:(Seg (k + 1)),(Seg (k + 1)):] by MATRIX_1:25;
len (Line ((B * A2) * C),1) = width ((B * A2) * C) by MATRIX_1:def 8
.= k + 1 by MATRIX_1:25 ;
then A102: len (Line ((B * A2) * C),1) = len (Base_FinSeq K,(k + 1),1) by Th23;
then A103: Line ((B * A2) * C),1 = Base_FinSeq K,(k + 1),1 by A15, FINSEQ_1:18;
A104: width F = k by MATRIX_1:25;
A105: 1 <= k + 1 by NAT_1:11;
len (Col B4,1) = len B4 by MATRIX_1:def 9
.= k + 1 by MATRIX_1:25 ;
then A106: len (Col B4,1) = len (Base_FinSeq K,(k + 1),1) by Th23;
then A107: Col B4,1 = Base_FinSeq K,(k + 1),1 by A92, FINSEQ_1:18;
for i, j being Nat st [i,j] in Indices (((B * A2) * C) * B4) holds
(((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j

proof

let i, j be Nat; :: thesis:
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 13;
A108: len (Line F,(i -' 1)) = width F by MATRIX_1:def 8
.= k by MATRIX_1:25 ;
A109: len (Col G2,(j -' 1)) = len G2 by MATRIX_1:def 9
.= k by MATRIX_1:25 ;
A110: len (Line ((B * A2) * C),i) = width ((B * A2) * C) by MATRIX_1:def 8
.= k + 1 by MATRIX_1:25 ;
A111: len (Col B4,j) = len B4 by MATRIX_1:def 9
.= k + 1 by MATRIX_1:25 ;
assume A112: [i,j] in Indices (((B * A2) * C) * B4) ; :: thesis:
then A113: [i,j] in [:(Seg (k + 1)),(Seg (k + 1)):] by MATRIX_1:25;
then A114: [i,j] in Indices (1. K,(k + 1)) by MATRIX_1:25;
A115: i in Seg (k + 1) by A101, A112, ZFMISC_1:106;
then A116: 1 <= i by FINSEQ_1:3;
A117: i <= k + 1 by A115, FINSEQ_1:3;
A118: j in Seg (k + 1) by A100, A112, ZFMISC_1:106;
then A119: 1 <= j by FINSEQ_1:3;
A120: len B4 = k + 1 by MATRIX_1:25;
A121: width ((B * A2) * C) = k + 1 by MATRIX_1:25;
A122: j <= k + 1 by A118, FINSEQ_1:3;
A123: [i,j] in Indices B4 by A101, A112, MATRIX_1:25;

now

per cases by A116, XXREAL_0:1;

suppose A124: i = 1 ; :: thesis:

now

per cases by A119, XXREAL_0:1;

suppose A125: j = 1 ; :: thesis:

(((B * A2) * C) * B4) * i,j = |((Line ((B * A2) * C),i0),(Col B4,j0))| by A112, A120, A121, MATRIX_3:def 4
.= 1. K by A103, A107, A105, A124, A125, Th36 ;
hence (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j by A114, A124, A125, MATRIX_1:def 12; :: thesis:

end;

suppose A126: j > 1 ; :: thesis:

1 <= len B4 by A105, MATRIX_1:25;
then A127: 1 in dom B4 by FINSEQ_3:27;
(((B * A2) * C) * B4) * i,j = |((Line ((B * A2) * C),i0),(Col B4,j0))| by A112, A120, A121, MATRIX_3:def 4
.= |((Base_FinSeq K,(k + 1),1),(Col B4,j0))| by A102, A15, A124, FINSEQ_1:18
.= |((Col B4,j0),(Base_FinSeq K,(k + 1),1))| by FVSUM_1:115
.= (Col B4,j0) . 1 by A105, A111, Th35
.= B4 * 1,j by A127, MATRIX_1:def 9
.= IFEQ i,1,(IFEQ j,1,(1. K),(0. K)),(IFEQ j,1,(0. K),(G2 * (i -' 1),(j -' 1))) by A89, A123, A124
.= IFEQ j,1,(1. K),(0. K) by A124, FUNCOP_1:def 8
.= 0. K by A126, FUNCOP_1:def 8 ;
hence (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j by A4, A113, A124, A126, MATRIX_1:def 12; :: thesis:

end;

hence (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j ; :: thesis:

end;

suppose A128: 1 < i ; :: thesis:

then A129: 1 + 1 <= i by NAT_1:13;

now

per cases by A119, XXREAL_0:1;

suppose A130: j = 1 ; :: thesis:

A131: 1 in Seg (width ((B * A2) * C)) by A14, A105, FINSEQ_1:3;
A132: len (Line ((B * A2) * C),i) = width ((B * A2) * C) by MATRIX_1:def 8
.= k + 1 by MATRIX_1:25 ;
(((B * A2) * C) * B4) * i,j = |((Line ((B * A2) * C),i0),(Col B4,j0))| by A112, A120, A121, MATRIX_3:def 4
.= |((Line ((B * A2) * C),i),(Base_FinSeq K,(k + 1),1))| by A106, A92, A130, FINSEQ_1:18
.= (Line ((B * A2) * C),i) . 1 by A105, A132, Th35
.= ((B * A2) * C) * i0,1 by A131, MATRIX_1:def 8
.= 0. K by A11, A117, A128 ;
hence (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j by A114, A128, A130, MATRIX_1:def 12; :: thesis:

end;

suppose A133: j > 1 ; :: thesis:

then 1 + 1 <= j by NAT_1:13;
then A134: 1 <= j - 1 by XREAL_1:21;
A135: i -' 1 = i - 1 by A128, XREAL_1:235;
then A136: i -' 1 <= k by A117, XREAL_1:22;
A137: 1 <= i - 1 by A129, XREAL_1:21;
then A138: i -' 1 in Seg k by A135, A136, FINSEQ_1:3;
A139: len (Line F,(i -' 1)) = width F by MATRIX_1:def 8
.= k by MATRIX_1:25 ;
A140: for k2 being Nat st k2 in dom (Line F,(i -' 1)) holds
(Line ((B * A2) * C),((i -' 1) + 1)) . ((len <*(0. K)*>) + k2) = (Line F,(i -' 1)) . k2

proof

let k2 be Nat; :: thesis:
assume A141: k2 in dom (Line F,(i -' 1)) ; :: thesis:
then A142: k2 in Seg (len (Line F,(i -' 1))) by FINSEQ_1:def 3;
then A143: k2 <= k by A139, FINSEQ_1:3;
then ( 1 <= k2 + 1 & k2 + 1 <= k + 1 ) by NAT_1:11, XREAL_1:9;
then A144: k2 + 1 in Seg (width ((B * A2) * C)) by A121, FINSEQ_1:3;
1 <= k2 by A142, FINSEQ_1:3;
then [(i -' 1),k2] in Indices F by A135, A137, A136, A143, MATRIX_1:38;
then A145: ((B * A2) * C) * ((i -' 1) + 1),(k2 + 1) = F * (i -' 1),k2 by A25;
k2 in Seg (width F) by A104, A139, A141, FINSEQ_1:def 3;
then ((B * A2) * C) * ((i -' 1) + 1),(k2 + 1) = (Line F,(i -' 1)) . k2 by A145, MATRIX_1:def 8;
then (Line ((B * A2) * C),((i -' 1) + 1)) . (k2 + 1) = (Line F,(i -' 1)) . k2 by A144, MATRIX_1:def 8;
hence (Line ((B * A2) * C),((i -' 1) + 1)) . ((len <*(0. K)*>) + k2) = (Line F,(i -' 1)) . k2 by FINSEQ_1:57; :: thesis:

end;

A146: for k2 being Nat st k2 in dom <*(0. K)*> holds
(Line ((B * A2) * C),((i -' 1) + 1)) . k2 = <*(0. K)*> . k2

proof

let k2 be Nat; :: thesis:
assume k2 in dom <*(0. K)*> ; :: thesis:
then k2 in Seg (len <*(0. K)*>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:4, FINSEQ_1:57;
then A147: k2 = 1 by TARSKI:def 1;
A148: ((B * A2) * C) * i0,1 = 0. K by A11, A117, A128;
1 <= k + 1 by NAT_1:11;
then k2 in Seg (width ((B * A2) * C)) by A121, A147, FINSEQ_1:3;
then (Line ((B * A2) * C),i) . k2 = 0. K by A147, A148, MATRIX_1:def 8;
hence (Line ((B * A2) * C),((i -' 1) + 1)) . k2 = <*(0. K)*> . k2 by A135, A147, FINSEQ_1:57; :: thesis:

end;

dom (Line ((B * A2) * C),((i -' 1) + 1)) = Seg (k + 1) by A110, A135, FINSEQ_1:def 3
.= Seg ((len <*(0. K)*>) + (len (Line F,(i -' 1)))) by A139, FINSEQ_1:56 ;
then A149: <*(0. K)*> ^ (Line F,(i -' 1)) = Line ((B * A2) * C),((i -' 1) + 1) by A146, A140, FINSEQ_1:def 7;
A150: (j -' 1) + 1 = (j - 1) + 1 by A133, XREAL_1:235
.= j ;
A151: j -' 1 = j - 1 by A133, XREAL_1:235;
then j -' 1 <= k by A122, XREAL_1:22;
then j -' 1 in Seg k by A151, A134, FINSEQ_1:3;
then A152: [(i -' 1),(j -' 1)] in [:(Seg k),(Seg k):] by A138, ZFMISC_1:106;
then A153: [(i -' 1),(j -' 1)] in Indices (F * G2) by MATRIX_1:25;
A154: for k2 being Nat st k2 in dom <*(0. K)*> holds
(Col B4,((j -' 1) + 1)) . k2 = <*(0. K)*> . k2

proof

1 <= 1 + k by NAT_1:11;
then [1,j] in Indices B4 by A119, A122, MATRIX_1:38;
then B4 * 1,j = IFEQ 1,1,(IFEQ j,1,(1. K),(0. K)),(IFEQ j,1,(0. K),(G2 * (1 -' 1),(j -' 1))) by A89;
then A155: B4 * 1,j = IFEQ j,1,(1. K),(0. K) by FUNCOP_1:def 8
.= 0. K by A133, FUNCOP_1:def 8 ;
let k2 be Nat; :: thesis:
assume k2 in dom <*(0. K)*> ; :: thesis:
then k2 in Seg (len <*(0. K)*>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:4, FINSEQ_1:57;
then A156: k2 = 1 by TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then k2 in Seg (len B4) by A120, A156, FINSEQ_1:3;
then k2 in dom B4 by FINSEQ_1:def 3;
then (Col B4,j) . k2 = 0. K by A156, A155, MATRIX_1:def 9;
hence (Col B4,((j -' 1) + 1)) . k2 = <*(0. K)*> . k2 by A151, A156, FINSEQ_1:57; :: thesis:

end;

A157: len (Col G2,(j -' 1)) = len G2 by MATRIX_1:def 9
.= k by MATRIX_1:25 ;
A158: for k2 being Nat st k2 in dom (Col G2,(j -' 1)) holds
(Col B4,((j -' 1) + 1)) . ((len <*(0. K)*>) + k2) = (Col G2,(j -' 1)) . k2

proof

let k2 be Nat; :: thesis:
assume A159: k2 in dom (Col G2,(j -' 1)) ; :: thesis:
then 1 <= k2 by FINSEQ_3:27;
then A160: 1 < k2 + 1 by NAT_1:13;
k2 in Seg k by A157, A159, FINSEQ_1:def 3;
then A161: k2 in dom G2 by A88, FINSEQ_1:def 3;
k2 <= k by A157, A159, FINSEQ_3:27;
then A162: ( 1 <= k2 + 1 & k2 + 1 <= k + 1 ) by NAT_1:11, XREAL_1:9;
then [(k2 + 1),j] in Indices B4 by A119, A122, MATRIX_1:38;
then B4 * (k2 + 1),j = IFEQ (k2 + 1),1,(IFEQ j,1,(1. K),(0. K)),(IFEQ j,1,(0. K),(G2 * ((k2 + 1) -' 1),(j -' 1))) by A89;
then B4 * (k2 + 1),j = IFEQ j,1,(0. K),(G2 * ((k2 + 1) -' 1),(j -' 1)) by A160, FUNCOP_1:def 8
.= G2 * ((k2 + 1) -' 1),(j -' 1) by A133, FUNCOP_1:def 8
.= G2 * k2,(j -' 1) by NAT_D:34 ;
then A163: B4 * (k2 + 1),((j -' 1) + 1) = (Col G2,(j -' 1)) . k2 by A151, A161, MATRIX_1:def 9;
k2 + 1 in dom B4 by A120, A162, FINSEQ_3:27;
then (Col B4,((j -' 1) + 1)) . (k2 + 1) = (Col G2,(j -' 1)) . k2 by A163, MATRIX_1:def 9;
hence (Col B4,((j -' 1) + 1)) . ((len <*(0. K)*>) + k2) = (Col G2,(j -' 1)) . k2 by FINSEQ_1:57; :: thesis:

end;

dom (Col B4,((j -' 1) + 1)) = Seg (len (Col B4,((j -' 1) + 1))) by FINSEQ_1:def 3
.= Seg ((len <*(0. K)*>) + (len (Col G2,(j -' 1)))) by A111, A151, A157, FINSEQ_1:56 ;
then A164: <*(0. K)*> ^ (Col G2,(j -' 1)) = Col B4,((j -' 1) + 1) by A154, A158, FINSEQ_1:def 7;
(i -' 1) + 1 = (i - 1) + 1 by A128, XREAL_1:235
.= i ;
then A165: (((B * A2) * C) * B4) * i,j = |((Line ((B * A2) * C),((i -' 1) + 1)),(Col B4,((j -' 1) + 1)))| by A112, A120, A121, A150, MATRIX_3:def 4
.= |(<*(0. K)*>,<*(0. K)*>)| + |((Line F,(i -' 1)),(Col G2,(j -' 1)))| by A23, A108, A109, A149, A164, Th12
.= (0. K) + |((Line F,(i -' 1)),(Col G2,(j -' 1)))| by Th22
.= (0. K) + ((F * G2) * (i -' 1),(j -' 1)) by A104, A88, A153, MATRIX_3:def 4
.= (1. K,k) * (i -' 1),(j -' 1) by A87, RLVECT_1:10 ;
A166: [(i -' 1),(j -' 1)] in Indices (1. K,k) by A152, MATRIX_1:25;

now

per cases ;

suppose A167: i = j ; :: thesis:

then (1. K,(k + 1)) * i0,j0 = 1. K by A114, MATRIX_1:def 12;
hence (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j by A166, A165, A167, MATRIX_1:def 12; :: thesis:

end;

suppose A168: i <> j ; :: thesis:

then i - 1 <> j - 1 ;
then i0 -' 1 <> j0 -' 1 by A128, A151, XREAL_1:235;
then (1. K,k) * (i0 -' 1),(j0 -' 1) = 0. K by A166, MATRIX_1:def 12;
hence (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j by A114, A165, A168, MATRIX_1:def 12; :: thesis:

end;

hence (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j ; :: thesis:

end;

hence (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j ; :: thesis:

end;

hence (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j ; :: thesis:

end;

then ( width (Inv B) = k + 1 & ((B * A2) * C) * B4 = 1. K,(k + 1) ) by MATRIX_1:25, MATRIX_1:28;
then (Inv B) * (((B * A2) * C) * B4) = Inv B by MATRIXR2:67;
then ((Inv B) * (((B * A2) * C) * B4)) * B = 1. K,(k + 1) by A8, Th18;
then ((Inv B) * ((B * A2) * (C * B4))) * B = 1. K,(k + 1) by Th17;
then ((Inv B) * (B * (A2 * (C * B4)))) * B = 1. K,(k + 1) by Th17;
then (((Inv B) * B) * (A2 * (C * B4))) * B = 1. K,(k + 1) by Th17;
then ( len (A2 * (C * B4)) = k + 1 & ((1. K,(k + 1)) * (A2 * (C * B4))) * B = 1. K,(k + 1) ) by A8, Th18, MATRIX_1:25;
then (A2 * (C * B4)) * B = 1. K,(k + 1) by MATRIXR2:68;
then A2 * ((C * B4) * B) = 1. K,(k + 1) by Th17;
hence ex B4 being Matrix of k + 1,K st A2 * B4 = 1. K,(k + 1) ; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

for D, B0 being Matrix of 0 ,K st B0 * D = 1. K,0 holds
ex B1 being Matrix of 0 ,K st D * B1 = 1. K,0

proof

let D, B0 be Matrix of 0 ,K; :: thesis:
assume B0 * D = 1. K,0 ; :: thesis:
D * (0. K,0 ) = 1. K,0 by Th15;
hence ex B1 being Matrix of 0 ,K st D * B1 = 1. K,0 ; :: thesis:

end;

then A169: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A169, A2);
hence ex B2 being Matrix of n,K st A * B2 = 1. K,n by A1; :: thesis:

end;