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:24;
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:6;
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:24;
A14: width ((B * A2) * C) = k + 1 by MATRIX_1:24;
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 7;
len (Line (((B * A2) * C),1)) = width ((B * A2) * C) by MATRIX_1:def 7;
then A19: j in Seg (width ((B * A2) * C)) by A16, A17, FINSEQ_1:1;

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 7;
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 12;
(Line (((B * A2) * C),1)) . j = ((B * A2) * C) * (1,j) by A19, MATRIX_1:def 7
.= 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:40;
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:24;
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:24;
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:24;
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:24;
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 8
.= k + 1 by MATRIX_1:24 ;
A34: len ((B * A2) * C) = k + 1 by MATRIX_1:24;
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 12;

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:1;
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 8; :: thesis:

end;

A41: len (Line ((((C ~) * B2) * (B ~)),i)) = width (((C ~) * B2) * (B ~)) by MATRIX_1:def 7
.= k + 1 by MATRIX_1:24 ;
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:24;
then A45: 1 in Seg (width (((C ~) * B2) * (B ~))) by A43, FINSEQ_1:1;
[i,1] in Indices ((((C ~) * B2) * (B ~)) * ((B * A2) * C)) by A42, A43, MATRIX_1:37;
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:14
.= (Line ((((C ~) * B2) * (B ~)),i)) . 1 by A43, A41, Th35
.= (((C ~) * B2) * (B ~)) * (i,1) by A45, MATRIX_1:def 7 ;
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:37;
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:7;
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:2, FINSEQ_1:40;
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:1;
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 8;
hence (Col (((B * A2) * C),(j + 1))) . k2 = <*(0. K)*> . k2 by A53, FINSEQ_1:40; :: thesis:

end;

A54: len (Col (F,j)) = len F by MATRIX_1:def 8
.= k by MATRIX_1:24 ;
A55: i + 1 <= k + 1 by A47, XREAL_1:7;
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:37;
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 11 ;
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:2, FINSEQ_1:40;
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:1;
then (Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = 0. K by A60, A59, MATRIX_1:def 7;
hence (Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = <*(0. K)*> . k2 by A60, FINSEQ_1:40; :: 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 8;
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:1;
then ( 1 <= k2 + 1 & k2 + 1 <= k + 1 ) by NAT_1:11, XREAL_1:7;
then A67: k2 + 1 in dom ((B * A2) * C) by A29, FINSEQ_3:25;
1 <= k2 by A65, FINSEQ_1:1;
then [k2,j] in Indices F by A48, A49, A66, MATRIX_1:37;
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 8;
hence (Col (((B * A2) * C),(j + 1))) . ((len <*(0. K)*>) + k2) = (Col (F,j)) . k2 by A23, A63, A67, MATRIX_1:def 8; :: thesis:

end;

A69: len (Line (G,i)) = width G by MATRIX_1:def 7
.= k by MATRIX_1:24 ;
A70: k + 1 = (len <*(0. K)*>) + k by FINSEQ_1:39;
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:24, 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 7
.= k by MATRIX_1:24 ;
then A76: k2 <= k by A74, FINSEQ_1:1;
1 <= k2 by A74, FINSEQ_1:1;
then [i,k2] in Indices G by A46, A47, A76, MATRIX_1:37;
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:24;
then A78: (((C ~) * B2) * (B ~)) * ((i + 1),(k2 + 1)) = (Line (G,i)) . k2 by A77, MATRIX_1:def 7;
k2 + 1 <= k + 1 by A76, XREAL_1:7;
then k2 + 1 in Seg (width (((C ~) * B2) * (B ~))) by A72, FINSEQ_1:1;
then (Line ((((C ~) * B2) * (B ~)),(i + 1))) . (k2 + 1) = (Line (G,i)) . k2 by A78, MATRIX_1:def 7;
hence (Line ((((C ~) * B2) * (B ~)),(i + 1))) . ((len <*(0. K)*>) + k2) = (Line (G,i)) . k2 by FINSEQ_1:40; :: thesis:

end;

A79: width G = k by MATRIX_1:24;
( len (Line ((((C ~) * B2) * (B ~)),(i + 1))) = width (((C ~) * B2) * (B ~)) & len (Line (G,i)) = width G ) by MATRIX_1:def 7;
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:7;

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:37;
then (1. (K,(k + 1))) * ((i + 1),(j + 1)) = 1. K by A84, MATRIX_1:def 11;
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:37;
then ( i + 1 <> j + 1 implies (1. (K,(k + 1))) * ((i + 1),(j + 1)) = 0. K ) by MATRIX_1:def 11;
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 8;
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:37;
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:4 ;
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:24;
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:24;
A91: width B4 = k + 1 by MATRIX_1:24;
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 8;
then 1 <= k + 1 by A93, XXREAL_0:2;
then A96: [j,1] in Indices B4 by A93, A95, MATRIX_1:37;
len (Col (B4,1)) = len B4 by MATRIX_1:def 8;
then j in Seg (width B4) by A90, A91, A93, A94, FINSEQ_1:1;
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 8
.= 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 8
.= 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:24;
A101: Indices (((B * A2) * C) * B4) = [:(Seg (k + 1)),(Seg (k + 1)):] by MATRIX_1:24;
len (Line (((B * A2) * C),1)) = width ((B * A2) * C) by MATRIX_1:def 7
.= k + 1 by MATRIX_1:24 ;
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:14;
A104: width F = k by MATRIX_1:24;
A105: 1 <= k + 1 by NAT_1:11;
len (Col (B4,1)) = len B4 by MATRIX_1:def 8
.= k + 1 by MATRIX_1:24 ;
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:14;
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 12;
A108: len (Line (F,(i -' 1))) = width F by MATRIX_1:def 7
.= k by MATRIX_1:24 ;
A109: len (Col (G2,(j -' 1))) = len G2 by MATRIX_1:def 8
.= k by MATRIX_1:24 ;
A110: len (Line (((B * A2) * C),i)) = width ((B * A2) * C) by MATRIX_1:def 7
.= k + 1 by MATRIX_1:24 ;
A111: len (Col (B4,j)) = len B4 by MATRIX_1:def 8
.= k + 1 by MATRIX_1:24 ;
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:24;
then A114: [i,j] in Indices (1. (K,(k + 1))) by MATRIX_1:24;
A115: i in Seg (k + 1) by A101, A112, ZFMISC_1:87;
then A116: 1 <= i by FINSEQ_1:1;
A117: i <= k + 1 by A115, FINSEQ_1:1;
A118: j in Seg (k + 1) by A100, A112, ZFMISC_1:87;
then A119: 1 <= j by FINSEQ_1:1;
A120: len B4 = k + 1 by MATRIX_1:24;
A121: width ((B * A2) * C) = k + 1 by MATRIX_1:24;
A122: j <= k + 1 by A118, FINSEQ_1:1;
A123: [i,j] in Indices B4 by A101, A112, MATRIX_1:24;

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 11; :: thesis:

end;

suppose A126: j > 1 ; :: thesis:

1 <= len B4 by A105, MATRIX_1:24;
then A127: 1 in dom B4 by FINSEQ_3:25;
(((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:14
.= |((Col (B4,j0)),(Base_FinSeq (K,(k + 1),1)))| by FVSUM_1:90
.= (Col (B4,j0)) . 1 by A105, A111, Th35
.= B4 * (1,j) by A127, MATRIX_1:def 8
.= 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 11; :: 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:1;
A132: len (Line (((B * A2) * C),i)) = width ((B * A2) * C) by MATRIX_1:def 7
.= k + 1 by MATRIX_1:24 ;
(((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:14
.= (Line (((B * A2) * C),i)) . 1 by A105, A132, Th35
.= ((B * A2) * C) * (i0,1) by A131, MATRIX_1:def 7
.= 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 11; :: thesis:

end;

suppose A133: j > 1 ; :: thesis:

then 1 + 1 <= j by NAT_1:13;
then A134: 1 <= j - 1 by XREAL_1:19;
A135: i -' 1 = i - 1 by A128, XREAL_1:233;
then A136: i -' 1 <= k by A117, XREAL_1:20;
A137: 1 <= i - 1 by A129, XREAL_1:19;
then A138: i -' 1 in Seg k by A135, A136, FINSEQ_1:1;
A139: len (Line (F,(i -' 1))) = width F by MATRIX_1:def 7
.= k by MATRIX_1:24 ;
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:1;
then ( 1 <= k2 + 1 & k2 + 1 <= k + 1 ) by NAT_1:11, XREAL_1:7;
then A144: k2 + 1 in Seg (width ((B * A2) * C)) by A121, FINSEQ_1:1;
1 <= k2 by A142, FINSEQ_1:1;
then [(i -' 1),k2] in Indices F by A135, A137, A136, A143, MATRIX_1:37;
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 7;
then (Line (((B * A2) * C),((i -' 1) + 1))) . (k2 + 1) = (Line (F,(i -' 1))) . k2 by A144, MATRIX_1:def 7;
hence (Line (((B * A2) * C),((i -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Line (F,(i -' 1))) . k2 by FINSEQ_1:40; :: 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:2, FINSEQ_1:40;
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:1;
then (Line (((B * A2) * C),i)) . k2 = 0. K by A147, A148, MATRIX_1:def 7;
hence (Line (((B * A2) * C),((i -' 1) + 1))) . k2 = <*(0. K)*> . k2 by A135, A147, FINSEQ_1:40; :: 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:39 ;
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:233
.= j ;
A151: j -' 1 = j - 1 by A133, XREAL_1:233;
then j -' 1 <= k by A122, XREAL_1:20;
then j -' 1 in Seg k by A151, A134, FINSEQ_1:1;
then A152: [(i -' 1),(j -' 1)] in [:(Seg k),(Seg k):] by A138, ZFMISC_1:87;
then A153: [(i -' 1),(j -' 1)] in Indices (F * G2) by MATRIX_1:24;
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:37;
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:2, FINSEQ_1:40;
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:1;
then k2 in dom B4 by FINSEQ_1:def 3;
then (Col (B4,j)) . k2 = 0. K by A156, A155, MATRIX_1:def 8;
hence (Col (B4,((j -' 1) + 1))) . k2 = <*(0. K)*> . k2 by A151, A156, FINSEQ_1:40; :: thesis:

end;

A157: len (Col (G2,(j -' 1))) = len G2 by MATRIX_1:def 8
.= k by MATRIX_1:24 ;
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:25;
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:25;
then A162: ( 1 <= k2 + 1 & k2 + 1 <= k + 1 ) by NAT_1:11, XREAL_1:7;
then [(k2 + 1),j] in Indices B4 by A119, A122, MATRIX_1:37;
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 8;
k2 + 1 in dom B4 by A120, A162, FINSEQ_3:25;
then (Col (B4,((j -' 1) + 1))) . (k2 + 1) = (Col (G2,(j -' 1))) . k2 by A163, MATRIX_1:def 8;
hence (Col (B4,((j -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Col (G2,(j -' 1))) . k2 by FINSEQ_1:40; :: 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:39 ;
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:233
.= 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:4 ;
A166: [(i -' 1),(j -' 1)] in Indices (1. (K,k)) by A152, MATRIX_1:24;

now

per cases ;

suppose A167: i = j ; :: thesis:

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

end;

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

then i - 1 <> j - 1 ;
then i0 -' 1 <> j0 -' 1 by A128, A151, XREAL_1:233;
then (1. (K,k)) * ((i0 -' 1),(j0 -' 1)) = 0. K by A166, MATRIX_1:def 11;
hence (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j) by A114, A165, A168, MATRIX_1:def 11; :: 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:24, MATRIX_1:27;
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:24;
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;