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

proof

defpred S₁[ 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: ex B2 being Matrix of n,K st A * B2 = 1. (K,n)
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
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: ( B2 * A2 = 1. (K,(k + 1)) implies ex B4 being Matrix of k + 1,K st A2 * B4 = 1. (K,(k + 1)) )
A4: Indices (1. (K,(k + 1))) = [:(Seg (k + 1)),(Seg (k + 1)):] by MATRIX_0:24;
assume A5: B2 * A2 = 1. (K,(k + 1)) ; :: thesis: ex B4 being Matrix of k + 1,K st A2 * B4 = 1. (K,(k + 1))
then A6: (Det B2) * (Det A2) = Det (1. (K,(k + 1))) by MATRIXR2:45;

now :: thesis: not A2 = 0. (K,(k + 1))

assume A2 = 0. (K,(k + 1)) ; :: thesis: contradiction
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 ;
not 0. K = 1_ K ;
hence contradiction by A6, A7, MATRIX_7:16, NAT_1:12; :: thesis: verum

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_0:24;
A14: width ((B * A2) * C) = k + 1 by MATRIX_0: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: ( 1 <= j & j <= len (Line (((B * A2) * C),1)) implies (Line (((B * A2) * C),1)) . j = (Base_FinSeq (K,(k + 1),1)) . j )
assume that
A16: 1 <= j and
A17: j <= len (Line (((B * A2) * C),1)) ; :: thesis: (Line (((B * A2) * C),1)) . j = (Base_FinSeq (K,(k + 1),1)) . j
A18: j <= k + 1 by A14, A17, MATRIX_0:def 7;
len (Line (((B * A2) * C),1)) = width ((B * A2) * C) by MATRIX_0:def 7;
then A19: j in Seg (width ((B * A2) * C)) by A16, A17, FINSEQ_1:1;

per cases ( 1 = j or 1 < j ) by A16, XXREAL_0:1;

suppose A20: 1 = j ; :: thesis: (Line (((B * A2) * C),1)) . j = (Base_FinSeq (K,(k + 1),1)) . j

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

end;

suppose A21: 1 < j ; :: thesis: (Line (((B * A2) * C),1)) . j = (Base_FinSeq (K,(k + 1),1)) . j

A22: j in NAT by ORDINAL1:def 12;
(Line (((B * A2) * C),1)) . j = ((B * A2) * C) * (1,j) by A19, MATRIX_0: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: verum

end;

end;

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_0: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_0:sch 1();
A26: len F = k by MATRIX_0: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_0: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_0:sch 1();
A29: len ((B * A2) * C) = k + 1 by MATRIX_0: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: ( 1 < i & i <= k + 1 implies (((C ~) * B2) * (B ~)) * (i,1) = (1. (K,(k + 1))) * (i,1) )
A33: len (Col (((B * A2) * C),1)) = len ((B * A2) * C) by MATRIX_0:def 8
.= k + 1 by MATRIX_0:24 ;
A34: len ((B * A2) * C) = k + 1 by MATRIX_0: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: ( 1 <= k2 & k2 <= len (Col (((B * A2) * C),1)) implies (Col (((B * A2) * C),1)) . k2 = (Base_FinSeq (K,(k + 1),1)) . k2 )
assume that
A36: 1 <= k2 and
A37: k2 <= len (Col (((B * A2) * C),1)) ; :: thesis: (Col (((B * A2) * C),1)) . k2 = (Base_FinSeq (K,(k + 1),1)) . k2
A38: k2 in NAT by ORDINAL1:def 12;

A39: now :: thesis: ((B * A2) * C) * (k2,1) = (Base_FinSeq (K,(k + 1),1)) . k2

per cases ( k2 = 1 or 1 < k2 ) by A36, XXREAL_0:1;

suppose k2 = 1 ; :: thesis: ((B * A2) * C) * (k2,1) = (Base_FinSeq (K,(k + 1),1)) . k2

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

end;

suppose A40: 1 < k2 ; :: thesis: ((B * A2) * C) * (k2,1) = (Base_FinSeq (K,(k + 1),1)) . k2

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: verum

end;

end;

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_0:def 8; :: thesis: verum

end;

A41: len (Line ((((C ~) * B2) * (B ~)),i)) = width (((C ~) * B2) * (B ~)) by MATRIX_0:def 7
.= k + 1 by MATRIX_0:24 ;
assume A42: ( 1 < i & i <= k + 1 ) ; :: thesis: (((C ~) * B2) * (B ~)) * (i,1) = (1. (K,(k + 1))) * (i,1)
then A43: 1 <= k + 1 by XXREAL_0:2;
A44: width (((C ~) * B2) * (B ~)) = k + 1 by MATRIX_0: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_0:31;
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_0:def 7 ;
hence (((C ~) * B2) * (B ~)) * (i,1) = (1. (K,(k + 1))) * (i,1) by A30; :: thesis: verum

end;

A46: k in NAT by ORDINAL1:def 12;
for i, j being 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 Nat; :: thesis: ( 1 <= i & i <= k & 1 <= j & j <= k implies (G * F) * (i,j) = IFEQ (i,j,(1. K),(0. K)) )
assume that
A47: 1 <= i and
A48: i <= k and
A49: 1 <= j and
A50: j <= k ; :: thesis: (G * F) * (i,j) = IFEQ (i,j,(1. K),(0. K))
A51: [i,j] in Indices (G * F) by A47, A48, A49, A50, MATRIX_0:31;
A52: 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 A49, A50, NAT_1:13, XREAL_1:7;
then A53: ((B * A2) * C) * (1,(j + 1)) = 0. K by A12;
let k2 be Nat; :: thesis: ( k2 in dom <*(0. K)*> implies (Col (((B * A2) * C),(j + 1))) . k2 = <*(0. K)*> . k2 )
assume k2 in dom <*(0. K)*> ; :: thesis: (Col (((B * A2) * C),(j + 1))) . k2 = <*(0. K)*> . k2
then k2 in Seg (len <*(0. K)*>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:2, FINSEQ_1:40;
then A54: k2 = 1 by TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then k2 in Seg (len ((B * A2) * C)) by A29, A54, 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 A54, A53, MATRIX_0:def 8;
hence (Col (((B * A2) * C),(j + 1))) . k2 = <*(0. K)*> . k2 by A54; :: thesis: verum

end;

A55: len (Col (F,j)) = len F by MATRIX_0:def 8
.= k by MATRIX_0:24 ;
A56: i + 1 <= k + 1 by A48, XREAL_1:7;
A57: 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: ( k2 in dom <*(0. K)*> implies (Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = <*(0. K)*> . k2 )
A58: 1 < i + 1 by A47, NAT_1:13;
1 <= 1 + k by NAT_1:11;
then A59: [(i + 1),1] in Indices (1. (K,(k + 1))) by A56, A58, MATRIX_0:31;
A60: (((C ~) * B2) * (B ~)) * ((i + 1),1) = (1. (K,(k + 1))) * ((i + 1),1) by A31, A56, A58
.= 0. K by A58, A59, MATRIX_1:def 3 ;
assume k2 in dom <*(0. K)*> ; :: thesis: (Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = <*(0. K)*> . k2
then k2 in Seg (len <*(0. K)*>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:2, FINSEQ_1:40;
then A61: k2 = 1 by TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then k2 in Seg (width (((C ~) * B2) * (B ~))) by A13, A61, FINSEQ_1:1;
then (Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = 0. K by A61, A60, MATRIX_0:def 7;
hence (Line ((((C ~) * B2) * (B ~)),(i + 1))) . k2 = <*(0. K)*> . k2 by A61; :: thesis: verum

end;

A62: 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: ( k2 in dom (Col (F,j)) implies (Col (((B * A2) * C),(j + 1))) . ((len <*(0. K)*>) + k2) = (Col (F,j)) . k2 )
A63: len (Col (F,(j0 -' 1))) = len F by MATRIX_0:def 8;
A64: j0 -' 1 = j by NAT_D:34;
assume A65: k2 in dom (Col (F,j)) ; :: thesis: (Col (((B * A2) * C),(j + 1))) . ((len <*(0. K)*>) + k2) = (Col (F,j)) . k2
then A66: k2 in Seg (len (Col (F,(j0 -' 1)))) by A64, FINSEQ_1:def 3;
then A67: k2 <= k by A26, A63, FINSEQ_1:1;
then ( 1 <= k2 + 1 & k2 + 1 <= k + 1 ) by NAT_1:11, XREAL_1:7;
then A68: k2 + 1 in dom ((B * A2) * C) by A29, FINSEQ_3:25;
1 <= k2 by A66, FINSEQ_1:1;
then [k2,j] in Indices F by A49, A50, A67, MATRIX_0:31;
then [k2,(j0 -' 1)] in Indices F by NAT_D:34;
then A69: ((B * A2) * C) * ((k2 + 1),((j0 -' 1) + 1)) = F * (k2,(j0 -' 1)) by A25;
k2 in Seg k by A26, A65, A63, A64, 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 A69, MATRIX_0:def 8;
hence (Col (((B * A2) * C),(j + 1))) . ((len <*(0. K)*>) + k2) = (Col (F,j)) . k2 by A23, A64, A68, MATRIX_0:def 8; :: thesis: verum

end;

A70: len (Line (G,i)) = width G by MATRIX_0:def 7
.= k by MATRIX_0:24 ;
A71: k + 1 = (len <*(0. K)*>) + k by FINSEQ_1:39;
A72: 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: ( k2 in dom (Line (G,i)) implies (Line ((((C ~) * B2) * (B ~)),(i + 1))) . ((len <*(0. K)*>) + k2) = (Line (G,i)) . k2 )
A73: ( width (((C ~) * B2) * (B ~)) = k + 1 & 1 <= k2 + 1 ) by MATRIX_0:24, NAT_1:11;
assume A74: k2 in dom (Line (G,i)) ; :: thesis: (Line ((((C ~) * B2) * (B ~)),(i + 1))) . ((len <*(0. K)*>) + k2) = (Line (G,i)) . k2
then A75: k2 in Seg (len (Line (G,i))) by FINSEQ_1:def 3;
A76: len (Line (G,i)) = width G by MATRIX_0:def 7
.= k by MATRIX_0:24 ;
then A77: k2 <= k by A75, FINSEQ_1:1;
1 <= k2 by A75, FINSEQ_1:1;
then [i,k2] in Indices G by A47, A48, A77, MATRIX_0:31;
then A78: (((C ~) * B2) * (B ~)) * ((i + 1),(k2 + 1)) = G * (i,k2) by A28;
k2 in Seg k by A74, A76, FINSEQ_1:def 3;
then k2 in Seg (width G) by MATRIX_0:24;
then A79: (((C ~) * B2) * (B ~)) * ((i + 1),(k2 + 1)) = (Line (G,i)) . k2 by A78, MATRIX_0:def 7;
k2 + 1 <= k + 1 by A77, XREAL_1:7;
then k2 + 1 in Seg (width (((C ~) * B2) * (B ~))) by A73, FINSEQ_1:1;
then (Line ((((C ~) * B2) * (B ~)),(i + 1))) . (k2 + 1) = (Line (G,i)) . k2 by A79, MATRIX_0:def 7;
hence (Line ((((C ~) * B2) * (B ~)),(i + 1))) . ((len <*(0. K)*>) + k2) = (Line (G,i)) . k2 by FINSEQ_1:40; :: thesis: verum

end;

A80: width G = k by MATRIX_0:24;
( len (Line ((((C ~) * B2) * (B ~)),(i + 1))) = width (((C ~) * B2) * (B ~)) & len (Line (G,i)) = width G ) by MATRIX_0:def 7;
then dom (Line ((((C ~) * B2) * (B ~)),(i + 1))) = Seg ((len <*(0. K)*>) + (len (Line (G,i)))) by A13, A80, A71, FINSEQ_1:def 3;
then A81: <*(0. K)*> ^ (Line (G,i)) = Line ((((C ~) * B2) * (B ~)),(i + 1)) by A57, A72, FINSEQ_1:def 7;
A82: ( 1 <= i + 1 & 1 <= j + 1 ) by NAT_1:11;
A83: j + 1 <= k + 1 by A50, XREAL_1:7;

A84: now :: thesis: (1. (K,(k + 1))) * ((i + 1),(j + 1)) = IFEQ (i,j,(1. K),(0. K))

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

suppose A85: i = j ; :: thesis: (1. (K,(k + 1))) * ((i + 1),(j + 1)) = IFEQ (i,j,(1. K),(0. K))

[(i + 1),(j + 1)] in Indices (1. (K,(k + 1))) by A82, A56, A83, MATRIX_0:31;
then (1. (K,(k + 1))) * ((i + 1),(j + 1)) = 1. K by A85, MATRIX_1:def 3;
hence (1. (K,(k + 1))) * ((i + 1),(j + 1)) = IFEQ (i,j,(1. K),(0. K)) by A85, FUNCOP_1:def 8; :: thesis: verum

end;

suppose A86: i <> j ; :: thesis: (1. (K,(k + 1))) * ((i + 1),(j + 1)) = IFEQ (i,j,(1. K),(0. K))

[(i + 1),(j + 1)] in Indices (1. (K,(k + 1))) by A82, A56, A83, MATRIX_0:31;
then ( i + 1 <> j + 1 implies (1. (K,(k + 1))) * ((i + 1),(j + 1)) = 0. K ) by MATRIX_1:def 3;
hence (1. (K,(k + 1))) * ((i + 1),(j + 1)) = IFEQ (i,j,(1. K),(0. K)) by A86, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

( len (Col (((B * A2) * C),(j + 1))) = len ((B * A2) * C) & len (Col (F,j)) = len F ) by MATRIX_0:def 8;
then dom (Col (((B * A2) * C),(j + 1))) = Seg ((len <*(0. K)*>) + (len (Col (F,j)))) by A29, A26, A71, FINSEQ_1:def 3;
then A87: <*(0. K)*> ^ (Col (F,j)) = Col (((B * A2) * C),(j + 1)) by A52, A62, FINSEQ_1:def 7;
[(i + 1),(j + 1)] in Indices ((((C ~) * B2) * (B ~)) * ((B * A2) * C)) by A82, A56, A83, MATRIX_0:31;
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, A81, A87, A70, A55, 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, A51, A80, A84, MATRIX_3:def 4; :: thesis: verum

end;

then G * F = 1. (K,k) by Th29, A46;
then consider G2 being Matrix of k,K such that
A88: 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))))));
A89: len G2 = k by MATRIX_0:24;
consider B4 being Matrix of k + 1,k + 1,K such that
A90: for i, j being Nat st [i,j] in Indices B4 holds
B4 * (i,j) = H₃(i,j) from MATRIX_0:sch 1();
A91: len B4 = k + 1 by MATRIX_0:24;
A92: width B4 = k + 1 by MATRIX_0:24;
A93: 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: ( 1 <= j & j <= len (Col (B4,1)) implies (Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j )
assume that
A94: 1 <= j and
A95: j <= len (Col (B4,1)) ; :: thesis: (Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j
A96: j <= k + 1 by A91, A95, MATRIX_0:def 8;
then 1 <= k + 1 by A94, XXREAL_0:2;
then A97: [j,1] in Indices B4 by A94, A96, MATRIX_0:31;
len (Col (B4,1)) = len B4 by MATRIX_0:def 8;
then j in Seg (width B4) by A91, A92, A94, A95, FINSEQ_1:1;
then A98: j in dom B4 by A91, A92, FINSEQ_1:def 3;

per cases ( 1 = j or 1 < j ) by A94, XXREAL_0:1;

suppose A99: 1 = j ; :: thesis: (Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j

(Col (B4,1)) . j = B4 * (j,1) by A98, MATRIX_0:def 8
.= IFEQ (j,1,(IFEQ (1,1,(1. K),(0. K))),(IFEQ (1,1,(0. K),(G2 * ((j -' 1),(1 -' 1)))))) by A90, A97
.= IFEQ (1,1,(1. K),(0. K)) by A99, FUNCOP_1:def 8
.= 1. K by FUNCOP_1:def 8 ;
hence (Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j by A96, A99, Th24; :: thesis: verum

end;

suppose A100: 1 < j ; :: thesis: (Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j

(Col (B4,1)) . j = B4 * (j,1) by A98, MATRIX_0:def 8
.= IFEQ (j,1,(IFEQ (1,1,(1. K),(0. K))),(IFEQ (1,1,(0. K),(G2 * ((j -' 1),(1 -' 1)))))) by A90, A97
.= IFEQ (1,1,(0. K),(G2 * ((j -' 1),(1 -' 1)))) by A100, FUNCOP_1:def 8
.= 0. K by FUNCOP_1:def 8 ;
hence (Col (B4,1)) . j = (Base_FinSeq (K,(k + 1),1)) . j by A96, A100, Th25; :: thesis: verum

end;

end;

end;

A101: width (((B * A2) * C) * B4) = k + 1 by MATRIX_0:24;
A102: Indices (((B * A2) * C) * B4) = [:(Seg (k + 1)),(Seg (k + 1)):] by MATRIX_0:24;
len (Line (((B * A2) * C),1)) = width ((B * A2) * C) by MATRIX_0:def 7
.= k + 1 by MATRIX_0:24 ;
then A103: len (Line (((B * A2) * C),1)) = len (Base_FinSeq (K,(k + 1),1)) by Th23;
then A104: Line (((B * A2) * C),1) = Base_FinSeq (K,(k + 1),1) by A15, FINSEQ_1:14;
A105: width F = k by MATRIX_0:24;
A106: 1 <= k + 1 by NAT_1:11;
len (Col (B4,1)) = len B4 by MATRIX_0:def 8
.= k + 1 by MATRIX_0:24 ;
then A107: len (Col (B4,1)) = len (Base_FinSeq (K,(k + 1),1)) by Th23;
then A108: Col (B4,1) = Base_FinSeq (K,(k + 1),1) by A93, 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: ( [i,j] in Indices (((B * A2) * C) * B4) implies (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j) )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def 12;
A109: len (Line (F,(i -' 1))) = width F by MATRIX_0:def 7
.= k by MATRIX_0:24 ;
A110: len (Col (G2,(j -' 1))) = len G2 by MATRIX_0:def 8
.= k by MATRIX_0:24 ;
A111: len (Line (((B * A2) * C),i)) = width ((B * A2) * C) by MATRIX_0:def 7
.= k + 1 by MATRIX_0:24 ;
A112: len (Col (B4,j)) = len B4 by MATRIX_0:def 8
.= k + 1 by MATRIX_0:24 ;
assume A113: [i,j] in Indices (((B * A2) * C) * B4) ; :: thesis: (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)
then A114: [i,j] in [:(Seg (k + 1)),(Seg (k + 1)):] by MATRIX_0:24;
then A115: [i,j] in Indices (1. (K,(k + 1))) by MATRIX_0:24;
A116: i in Seg (k + 1) by A102, A113, ZFMISC_1:87;
then A117: 1 <= i by FINSEQ_1:1;
A118: i <= k + 1 by A116, FINSEQ_1:1;
A119: j in Seg (k + 1) by A101, A113, ZFMISC_1:87;
then A120: 1 <= j by FINSEQ_1:1;
A121: len B4 = k + 1 by MATRIX_0:24;
A122: width ((B * A2) * C) = k + 1 by MATRIX_0:24;
A123: j <= k + 1 by A119, FINSEQ_1:1;
A124: [i,j] in Indices B4 by A102, A113, MATRIX_0:24;

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

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

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

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

per cases ( j = 1 or j > 1 ) by A120, XXREAL_0:1;

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

(((B * A2) * C) * B4) * (i,j) = |((Line (((B * A2) * C),i0)),(Col (B4,j0)))| by A113, A121, A122, MATRIX_3:def 4
.= 1. K by A104, A108, A106, A125, A126, Th36 ;
hence (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j) by A115, A125, A126, MATRIX_1:def 3; :: thesis: verum

end;

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

1 <= len B4 by A106, MATRIX_0:24;
then A128: 1 in dom B4 by FINSEQ_3:25;
(((B * A2) * C) * B4) * (i,j) = |((Line (((B * A2) * C),i0)),(Col (B4,j0)))| by A113, A121, A122, MATRIX_3:def 4
.= |((Base_FinSeq (K,(k + 1),1)),(Col (B4,j0)))| by A103, A15, A125, FINSEQ_1:14
.= |((Col (B4,j0)),(Base_FinSeq (K,(k + 1),1)))| by FVSUM_1:90
.= (Col (B4,j0)) . 1 by A106, A112, Th35
.= B4 * (1,j) by A128, MATRIX_0:def 8
.= IFEQ (i,1,(IFEQ (j,1,(1. K),(0. K))),(IFEQ (j,1,(0. K),(G2 * ((i -' 1),(j -' 1)))))) by A90, A124, A125
.= IFEQ (j,1,(1. K),(0. K)) by A125, FUNCOP_1:def 8
.= 0. K by A127, FUNCOP_1:def 8 ;
hence (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j) by A4, A114, A125, A127, MATRIX_1:def 3; :: thesis: verum

end;

end;

end;

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

end;

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

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

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

per cases ( j = 1 or j > 1 ) by A120, XXREAL_0:1;

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

A132: 1 in Seg (width ((B * A2) * C)) by A14, A106, FINSEQ_1:1;
A133: len (Line (((B * A2) * C),i)) = width ((B * A2) * C) by MATRIX_0:def 7
.= k + 1 by MATRIX_0:24 ;
(((B * A2) * C) * B4) * (i,j) = |((Line (((B * A2) * C),i0)),(Col (B4,j0)))| by A113, A121, A122, MATRIX_3:def 4
.= |((Line (((B * A2) * C),i)),(Base_FinSeq (K,(k + 1),1)))| by A107, A93, A131, FINSEQ_1:14
.= (Line (((B * A2) * C),i)) . 1 by A106, A133, Th35
.= ((B * A2) * C) * (i0,1) by A132, MATRIX_0:def 7
.= 0. K by A11, A118, A129 ;
hence (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j) by A115, A129, A131, MATRIX_1:def 3; :: thesis: verum

end;

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

then 1 + 1 <= j by NAT_1:13;
then A135: 1 <= j - 1 by XREAL_1:19;
A136: i -' 1 = i - 1 by A129, XREAL_1:233;
then A137: i -' 1 <= k by A118, XREAL_1:20;
A138: 1 <= i - 1 by A130, XREAL_1:19;
then A139: i -' 1 in Seg k by A136, A137, FINSEQ_1:1;
A140: len (Line (F,(i -' 1))) = width F by MATRIX_0:def 7
.= k by MATRIX_0:24 ;
A141: 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: ( k2 in dom (Line (F,(i -' 1))) implies (Line (((B * A2) * C),((i -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Line (F,(i -' 1))) . k2 )
assume A142: k2 in dom (Line (F,(i -' 1))) ; :: thesis: (Line (((B * A2) * C),((i -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Line (F,(i -' 1))) . k2
then A143: k2 in Seg (len (Line (F,(i -' 1)))) by FINSEQ_1:def 3;
then A144: k2 <= k by A140, FINSEQ_1:1;
then ( 1 <= k2 + 1 & k2 + 1 <= k + 1 ) by NAT_1:11, XREAL_1:7;
then A145: k2 + 1 in Seg (width ((B * A2) * C)) by A122, FINSEQ_1:1;
1 <= k2 by A143, FINSEQ_1:1;
then [(i -' 1),k2] in Indices F by A136, A138, A137, A144, MATRIX_0:31;
then A146: ((B * A2) * C) * (((i -' 1) + 1),(k2 + 1)) = F * ((i -' 1),k2) by A25;
k2 in Seg (width F) by A105, A140, A142, FINSEQ_1:def 3;
then ((B * A2) * C) * (((i -' 1) + 1),(k2 + 1)) = (Line (F,(i -' 1))) . k2 by A146, MATRIX_0:def 7;
then (Line (((B * A2) * C),((i -' 1) + 1))) . (k2 + 1) = (Line (F,(i -' 1))) . k2 by A145, MATRIX_0:def 7;
hence (Line (((B * A2) * C),((i -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Line (F,(i -' 1))) . k2 by FINSEQ_1:40; :: thesis: verum

end;

A147: 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: ( k2 in dom <*(0. K)*> implies (Line (((B * A2) * C),((i -' 1) + 1))) . k2 = <*(0. K)*> . k2 )
assume k2 in dom <*(0. K)*> ; :: thesis: (Line (((B * A2) * C),((i -' 1) + 1))) . k2 = <*(0. K)*> . k2
then k2 in Seg (len <*(0. K)*>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:2, FINSEQ_1:40;
then A148: k2 = 1 by TARSKI:def 1;
A149: ((B * A2) * C) * (i0,1) = 0. K by A11, A118, A129;
1 <= k + 1 by NAT_1:11;
then k2 in Seg (width ((B * A2) * C)) by A122, A148, FINSEQ_1:1;
then (Line (((B * A2) * C),i)) . k2 = 0. K by A148, A149, MATRIX_0:def 7;
hence (Line (((B * A2) * C),((i -' 1) + 1))) . k2 = <*(0. K)*> . k2 by A136, A148; :: thesis: verum

end;

dom (Line (((B * A2) * C),((i -' 1) + 1))) = Seg (k + 1) by A111, A136, FINSEQ_1:def 3
.= Seg ((len <*(0. K)*>) + (len (Line (F,(i -' 1))))) by A140, FINSEQ_1:39 ;
then A150: <*(0. K)*> ^ (Line (F,(i -' 1))) = Line (((B * A2) * C),((i -' 1) + 1)) by A147, A141, FINSEQ_1:def 7;
A151: (j -' 1) + 1 = (j - 1) + 1 by A134, XREAL_1:233
.= j ;
A152: j -' 1 = j - 1 by A134, XREAL_1:233;
then j -' 1 <= k by A123, XREAL_1:20;
then j -' 1 in Seg k by A152, A135, FINSEQ_1:1;
then A153: [(i -' 1),(j -' 1)] in [:(Seg k),(Seg k):] by A139, ZFMISC_1:87;
then A154: [(i -' 1),(j -' 1)] in Indices (F * G2) by MATRIX_0:24;
A155: 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 A120, A123, MATRIX_0:31;
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 A90;
then A156: B4 * (1,j) = IFEQ (j,1,(1. K),(0. K)) by FUNCOP_1:def 8
.= 0. K by A134, FUNCOP_1:def 8 ;
let k2 be Nat; :: thesis: ( k2 in dom <*(0. K)*> implies (Col (B4,((j -' 1) + 1))) . k2 = <*(0. K)*> . k2 )
assume k2 in dom <*(0. K)*> ; :: thesis: (Col (B4,((j -' 1) + 1))) . k2 = <*(0. K)*> . k2
then k2 in Seg (len <*(0. K)*>) by FINSEQ_1:def 3;
then k2 in {1} by FINSEQ_1:2, FINSEQ_1:40;
then A157: k2 = 1 by TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then k2 in Seg (len B4) by A121, A157, FINSEQ_1:1;
then k2 in dom B4 by FINSEQ_1:def 3;
then (Col (B4,j)) . k2 = 0. K by A157, A156, MATRIX_0:def 8;
hence (Col (B4,((j -' 1) + 1))) . k2 = <*(0. K)*> . k2 by A152, A157; :: thesis: verum

end;

A158: len (Col (G2,(j -' 1))) = len G2 by MATRIX_0:def 8
.= k by MATRIX_0:24 ;
A159: 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: ( k2 in dom (Col (G2,(j -' 1))) implies (Col (B4,((j -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Col (G2,(j -' 1))) . k2 )
assume A160: k2 in dom (Col (G2,(j -' 1))) ; :: thesis: (Col (B4,((j -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Col (G2,(j -' 1))) . k2
then 1 <= k2 by FINSEQ_3:25;
then A161: 1 < k2 + 1 by NAT_1:13;
k2 in Seg k by A158, A160, FINSEQ_1:def 3;
then A162: k2 in dom G2 by A89, FINSEQ_1:def 3;
k2 <= k by A158, A160, FINSEQ_3:25;
then A163: ( 1 <= k2 + 1 & k2 + 1 <= k + 1 ) by NAT_1:11, XREAL_1:7;
then [(k2 + 1),j] in Indices B4 by A120, A123, MATRIX_0:31;
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 A90;
then B4 * ((k2 + 1),j) = IFEQ (j,1,(0. K),(G2 * (((k2 + 1) -' 1),(j -' 1)))) by A161, FUNCOP_1:def 8
.= G2 * (((k2 + 1) -' 1),(j -' 1)) by A134, FUNCOP_1:def 8
.= G2 * (k2,(j -' 1)) by NAT_D:34 ;
then A164: B4 * ((k2 + 1),((j -' 1) + 1)) = (Col (G2,(j -' 1))) . k2 by A152, A162, MATRIX_0:def 8;
k2 + 1 in dom B4 by A121, A163, FINSEQ_3:25;
then (Col (B4,((j -' 1) + 1))) . (k2 + 1) = (Col (G2,(j -' 1))) . k2 by A164, MATRIX_0:def 8;
hence (Col (B4,((j -' 1) + 1))) . ((len <*(0. K)*>) + k2) = (Col (G2,(j -' 1))) . k2 by FINSEQ_1:40; :: thesis: verum

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 A112, A152, A158, FINSEQ_1:39 ;
then A165: <*(0. K)*> ^ (Col (G2,(j -' 1))) = Col (B4,((j -' 1) + 1)) by A155, A159, FINSEQ_1:def 7;
(i -' 1) + 1 = (i - 1) + 1 by A129, XREAL_1:233
.= i ;
then A166: (((B * A2) * C) * B4) * (i,j) = |((Line (((B * A2) * C),((i -' 1) + 1))),(Col (B4,((j -' 1) + 1))))| by A113, A121, A122, A151, MATRIX_3:def 4
.= |(<*(0. K)*>,<*(0. K)*>)| + |((Line (F,(i -' 1))),(Col (G2,(j -' 1))))| by A23, A109, A110, A150, A165, Th12
.= (0. K) + |((Line (F,(i -' 1))),(Col (G2,(j -' 1))))| by Th22
.= (0. K) + ((F * G2) * ((i -' 1),(j -' 1))) by A105, A89, A154, MATRIX_3:def 4
.= (1. (K,k)) * ((i -' 1),(j -' 1)) by A88, RLVECT_1:4 ;
A167: [(i -' 1),(j -' 1)] in Indices (1. (K,k)) by A153, MATRIX_0:24;

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

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

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

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

end;

suppose A169: i <> j ; :: thesis: (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j)

then i - 1 <> j - 1 ;
then i0 -' 1 <> j0 -' 1 by A129, A152, XREAL_1:233;
then (1. (K,k)) * ((i0 -' 1),(j0 -' 1)) = 0. K by A167, MATRIX_1:def 3;
hence (((B * A2) * C) * B4) * (i,j) = (1. (K,(k + 1))) * (i,j) by A115, A166, A169, MATRIX_1:def 3; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

end;

end;

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

end;

then ( width (Inv B) = k + 1 & ((B * A2) * C) * B4 = 1. (K,(k + 1)) ) by MATRIX_0:24, MATRIX_0: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_0: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: verum

end;

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

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: ( B0 * D = 1. (K,0) implies ex B1 being Matrix of 0 ,K st D * B1 = 1. (K,0) )
assume B0 * D = 1. (K,0) ; :: thesis: ex B1 being Matrix of 0 ,K st D * B1 = 1. (K,0)
D * (0. (K,0)) = 1. (K,0) by Th15;
hence ex B1 being Matrix of 0 ,K st D * B1 = 1. (K,0) ; :: thesis: verum

end;

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

end;