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: verumproof
assume B1:
B * A = 1. K,
n
;
:: thesis: ex B2 being Matrix of n,K st A * B2 = 1. K,n
defpred S1[
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;
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 &
(0. K,0 ) * D = 1. K,
0 )
by AA4350;
hence
ex
B1 being
Matrix of
0 ,
K st
D * B1 = 1. K,
0
;
:: thesis: verum
end;
then B3:
S1[
0 ]
;
B4:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume C1:
S1[
k]
;
:: thesis: S1[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) )
assume D2:
B2 * A2 = 1. K,
(k + 1)
;
:: thesis: ex B4 being Matrix of k + 1,K st A2 * B4 = 1. K,(k + 1)
D8a:
(Det B2) * (Det A2) = Det (1. K,(k + 1))
by D2, MATRIXR2:45;
consider B,
C being
Matrix of
k + 1,
K such that D9:
(
B is
invertible &
C is
invertible &
((B * A2) * C) * 1,1
= 1. K & ( for
i being
Element of
NAT st 1
< i &
i <= k + 1 holds
((B * A2) * C) * i,1
= 0. K ) & ( for
j being
Element of
NAT st 1
< j &
j <= k + 1 holds
((B * A2) * C) * 1,
j = 0. K ) )
by AA4200, D6;
set A3 =
(B * A2) * C;
set B3 =
((C ~ ) * B2) * (B ~ );
A1e:
len (A2 * C) = k + 1
by MATRIX_1:25;
A1d:
len C = k + 1
by MATRIX_1:25;
D44:
(((C ~ ) * B2) * (B ~ )) * ((B * A2) * C) =
(((C ~ ) * B2) * (B ~ )) * (B * (A2 * C))
by AA41
.=
((((Inv C) * B2) * (Inv B)) * B) * (A2 * C)
by AA41
.=
(((Inv C) * B2) * ((Inv B) * B)) * (A2 * C)
by AA41
.=
(((Inv C) * B2) * (1. K,(k + 1))) * (A2 * C)
by D9, AA4140
.=
((Inv C) * B2) * ((1. K,(k + 1)) * (A2 * C))
by AA41
.=
((Inv C) * B2) * (A2 * C)
by A1e, MATRIXR2:68
.=
(((Inv C) * B2) * A2) * C
by AA41
.=
((Inv C) * (1. K,(k + 1))) * C
by D2, AA41
.=
(Inv C) * ((1. K,(k + 1)) * C)
by AA41
.=
(Inv C) * C
by A1d, MATRIXR2:68
.=
1. K,
(k + 1)
by AA4140, D9
;
D71:
for
i being
Nat st 1
< i &
i <= k + 1 holds
(((C ~ ) * B2) * (B ~ )) * i,1
= (1. K,(k + 1)) * i,1
proof
let i be
Nat;
:: thesis: ( 1 < i & i <= k + 1 implies (((C ~ ) * B2) * (B ~ )) * i,1 = (1. K,(k + 1)) * i,1 )
assume G1:
( 1
< i &
i <= k + 1 )
;
:: thesis: (((C ~ ) * B2) * (B ~ )) * i,1 = (1. K,(k + 1)) * i,1
then G2:
1
<= k + 1
by XXREAL_0:2;
E4b:
(
len (((C ~ ) * B2) * (B ~ )) = k + 1 &
width (((C ~ ) * B2) * (B ~ )) = k + 1 &
Indices (((C ~ ) * B2) * (B ~ )) = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
E4c:
(
len ((B * A2) * C) = k + 1 &
width ((B * A2) * C) = k + 1 &
Indices ((B * A2) * C) = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
G5:
len (Col ((B * A2) * C),1) =
len ((B * A2) * C)
by MATRIX_1:def 9
.=
k + 1
by MATRIX_1:25
;
G6:
len (Base_FinSeq K,(k + 1),1) = k + 1
by AA1100;
G6a:
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 )
B:
k2 in NAT
by ORDINAL1:def 13;
assume H1:
( 1
<= k2 &
k2 <= len (Col ((B * A2) * C),1) )
;
:: thesis: (Col ((B * A2) * C),1) . k2 = (Base_FinSeq K,(k + 1),1) . k2
then
k2 in Seg (len ((B * A2) * C))
by G5, E4c, FINSEQ_1:3;
then H2:
k2 in dom ((B * A2) * C)
by FINSEQ_1:def 3;
now per cases
( k2 = 1 or 1 < k2 )
by H1, XXREAL_0:1;
suppose I0:
1
< k2
;
:: thesis: ((B * A2) * C) * k2,1 = (Base_FinSeq K,(k + 1),1) . k2hence ((B * A2) * C) * k2,1 =
0. K
by B, D9, H1, G5
.=
(Base_FinSeq K,(k + 1),1) . k2
by I0, AA1120, G2, H1, G5
;
:: thesis: verum end;
hence
(Col ((B * A2) * C),1) . k2 = (Base_FinSeq K,(k + 1),1) . k2
by H2, MATRIX_1:def 9;
:: thesis: verum
end;
G9:
len (Line (((C ~ ) * B2) * (B ~ )),i) =
width (((C ~ ) * B2) * (B ~ ))
by MATRIX_1:def 8
.=
k + 1
by MATRIX_1:25
;
G10b:
1
in Seg (width (((C ~ ) * B2) * (B ~ )))
by E4b, G2, FINSEQ_1:3;
[i,1] in Indices ((((C ~ ) * B2) * (B ~ )) * ((B * A2) * C))
by G1, G2, MATRIX_1:38;
then ((((C ~ ) * B2) * (B ~ )) * ((B * A2) * C)) * i,1 =
|((Line (((C ~ ) * B2) * (B ~ )),i),(Col ((B * A2) * C),1))|
by E4b, E4c, MATRIX_3:def 4
.=
|((Line (((C ~ ) * B2) * (B ~ )),i),(Base_FinSeq K,(k + 1),1))|
by G5, G6, G6a, FINSEQ_1:18
.=
(Line (((C ~ ) * B2) * (B ~ )),i) . 1
by G2, G9, AA2627
.=
(((C ~ ) * B2) * (B ~ )) * i,1
by G10b, MATRIX_1:def 8
;
hence
(((C ~ ) * B2) * (B ~ )) * i,1
= (1. K,(k + 1)) * i,1
by D44;
:: thesis: verum
end;
deffunc H1(
Nat,
Nat)
-> Element of the
carrier of
K =
((B * A2) * C) * ($1 + 1),
($2 + 1);
consider F being
Matrix of
k,
k,
K such that D12:
for
i,
j being
Nat st
[i,j] in Indices F holds
F * i,
j = H1(
i,
j)
from MATRIX_1:sch 1();
deffunc H2(
Nat,
Nat)
-> Element of the
carrier of
K =
(((C ~ ) * B2) * (B ~ )) * ($1 + 1),
($2 + 1);
consider G being
Matrix of
k,
k,
K such that D13:
for
i,
j being
Nat st
[i,j] in Indices G holds
G * i,
j = H2(
i,
j)
from MATRIX_1:sch 1();
E30:
(
len (1. K,(k + 1)) = k + 1 &
width (1. K,(k + 1)) = k + 1 &
Indices (1. K,(k + 1)) = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
E4b:
(
len (((C ~ ) * B2) * (B ~ )) = k + 1 &
width (((C ~ ) * B2) * (B ~ )) = k + 1 &
Indices (((C ~ ) * B2) * (B ~ )) = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
E5b:
(
len ((B * A2) * C) = k + 1 &
width ((B * A2) * C) = k + 1 &
Indices ((B * A2) * C) = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
E5:
(
len F = k &
width F = k &
Indices F = [:(Seg k),(Seg k):] )
by MATRIX_1:25;
E22:
len <*(0. K)*> = 1
by FINSEQ_1:57;
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: ( 1 <= i & i <= k & 1 <= j & j <= k implies (G * F) * i,j = IFEQ i,j,(1. K),(0. K) )
assume E1:
( 1
<= i &
i <= k & 1
<= j &
j <= k )
;
:: thesis: (G * F) * i,j = IFEQ i,j,(1. K),(0. K)
E40:
len (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) = width (((C ~ ) * B2) * (B ~ ))
by MATRIX_1:def 8;
E40b:
len (Col ((B * A2) * C),(j + 1)) = len ((B * A2) * C)
by MATRIX_1:def 9;
E45:
len (Line G,i) = width G
by MATRIX_1:def 8;
E46:
len (Col F,j) = len F
by MATRIX_1:def 9;
E12:
( 1
<= i + 1 & 1
<= j + 1 )
by NAT_1:11;
E13:
i + 1
<= k + 1
by E1, XREAL_1:9;
E13a:
j + 1
<= k + 1
by E1, XREAL_1:9;
E3:
[i,j] in Indices (G * F)
by E1, MATRIX_1:38;
E4:
(
len G = k &
width G = k &
Indices G = [:(Seg k),(Seg k):] )
by MATRIX_1:25;
E3b:
[(i + 1),(j + 1)] in Indices ((((C ~ ) * B2) * (B ~ )) * ((B * A2) * C))
by E12, E13, E13a, MATRIX_1:38;
E29:
k + 1
= (len <*(0. K)*>) + k
by FINSEQ_1:56;
then E30a:
dom (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) = Seg ((len <*(0. K)*>) + (len (Line G,i)))
by E4b, E40, E45, E4, FINSEQ_1:def 3;
E31:
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 )
assume F1a:
k2 in dom <*(0. K)*>
;
:: thesis: (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . k2 = <*(0. K)*> . k2
F1b:
k2 in Seg (len <*(0. K)*>)
by F1a, FINSEQ_1:def 3;
F1d:
k2 in {1}
by F1b, FINSEQ_1:4, FINSEQ_1:57;
F5:
k2 = 1
by F1d, TARSKI:def 1;
F1e:
1
<= 1
+ k
by NAT_1:11;
F8a:
1
<= k + 1
by NAT_1:11;
F12:
k2 in Seg (width (((C ~ ) * B2) * (B ~ )))
by F5, E4b, F8a, FINSEQ_1:3;
E12b:
1
< i + 1
by E1, NAT_1:13;
then F52:
[(i + 1),1] in Indices (1. K,(k + 1))
by F1e, E13, MATRIX_1:38;
(((C ~ ) * B2) * (B ~ )) * (i + 1),1 =
(1. K,(k + 1)) * (i + 1),1
by E12b, E13, D71
.=
0. K
by E12b, F52, MATRIX_1:def 12
;
then
(Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . k2 = 0. K
by F12, F5, MATRIX_1:def 8;
hence
(Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . k2 = <*(0. K)*> . k2
by F5, FINSEQ_1:57;
:: thesis: verum
end;
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 )
assume F1a:
k2 in dom (Line G,i)
;
:: thesis: (Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . ((len <*(0. K)*>) + k2) = (Line G,i) . k2
F1:
k2 in Seg (len (Line G,i))
by F1a, FINSEQ_1:def 3;
F1b:
len (Line G,i) =
width G
by MATRIX_1:def 8
.=
k
by MATRIX_1:25
;
F2:
( 1
<= k2 &
k2 <= k )
by F1, F1b, FINSEQ_1:3;
E4c:
(
len (((C ~ ) * B2) * (B ~ )) = k + 1 &
width (((C ~ ) * B2) * (B ~ )) = k + 1 &
Indices (((C ~ ) * B2) * (B ~ )) = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
F30f:
( 1
<= k2 + 1 &
k2 + 1
<= k + 1 )
by F2, NAT_1:11, XREAL_1:9;
F3:
k2 + 1
in Seg (width (((C ~ ) * B2) * (B ~ )))
by E4c, F30f, FINSEQ_1:3;
F30d:
[i,k2] in Indices G
by F2, E1, MATRIX_1:38;
F30:
(((C ~ ) * B2) * (B ~ )) * (i + 1),
(k2 + 1) = G * i,
k2
by D13, F30d;
F30a:
k2 in Seg k
by F1a, F1b, FINSEQ_1:def 3;
F30b:
k2 in Seg (width G)
by F30a, MATRIX_1:25;
F30c:
(((C ~ ) * B2) * (B ~ )) * (i + 1),
(k2 + 1) = (Line G,i) . k2
by F30, F30b, MATRIX_1:def 8;
(Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . (k2 + 1) = (Line G,i) . k2
by F3, F30c, MATRIX_1:def 8;
hence
(Line (((C ~ ) * B2) * (B ~ )),(i + 1)) . ((len <*(0. K)*>) + k2) = (Line G,i) . k2
by FINSEQ_1:57;
:: thesis: verum
end;
then E18:
<*(0. K)*> ^ (Line G,i) = Line (((C ~ ) * B2) * (B ~ )),
(i + 1)
by E30a, E31, FINSEQ_1:def 7;
E30b:
dom (Col ((B * A2) * C),(j + 1)) = Seg ((len <*(0. K)*>) + (len (Col F,j)))
by E5b, E29, E40b, E46, E5, FINSEQ_1:def 3;
E31b:
for
k2 being
Nat st
k2 in dom <*(0. K)*> holds
(Col ((B * A2) * C),(j + 1)) . k2 = <*(0. K)*> . k2
proof
let k2 be
Nat;
:: thesis: ( k2 in dom <*(0. K)*> implies (Col ((B * A2) * C),(j + 1)) . k2 = <*(0. K)*> . k2 )
assume F1a:
k2 in dom <*(0. K)*>
;
:: thesis: (Col ((B * A2) * C),(j + 1)) . k2 = <*(0. K)*> . k2
F1b:
k2 in Seg (len <*(0. K)*>)
by F1a, FINSEQ_1:def 3;
F1d:
k2 in {1}
by F1b, FINSEQ_1:4, FINSEQ_1:57;
F5:
k2 = 1
by F1d, TARSKI:def 1;
F16a:
1
<= k + 1
by NAT_1:11;
F16b:
k2 in Seg (len ((B * A2) * C))
by F5, E5b, F16a, FINSEQ_1:3;
F12:
k2 in dom ((B * A2) * C)
by F16b, FINSEQ_1:def 3;
F71:
( 1
<= j + 1 &
j + 1
<= k + 1 )
by E1, NAT_1:11, XREAL_1:9;
F1f:
1
< j + 1
by E1, NAT_1:13;
F1g:
((B * A2) * C) * 1,
(j + 1) = 0. K
by F71, D9, F1f;
(Col ((B * A2) * C),(j + 1)) . k2 = 0. K
by F12, F5, F1g, MATRIX_1:def 9;
hence
(Col ((B * A2) * C),(j + 1)) . k2 = <*(0. K)*> . k2
by F5, FINSEQ_1:57;
:: thesis: verum
end;
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
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 )
assume F0:
k2 in dom (Col F,j)
;
:: thesis: (Col ((B * A2) * C),(j + 1)) . ((len <*(0. K)*>) + k2) = (Col F,j) . k2
reconsider j0 =
j + 1 as
Element of
NAT ;
E46:
len (Col F,(j0 -' 1)) = len F
by MATRIX_1:def 9;
F33:
j0 -' 1
= j
by NAT_D:34;
F33a:
k2 in Seg (len (Col F,(j0 -' 1)))
by F0, F33, FINSEQ_1:def 3;
F2:
( 1
<= k2 &
k2 <= k )
by E5, E46, F33a, FINSEQ_1:3;
K11:
( 1
<= k2 + 1 &
k2 + 1
<= k + 1 )
by F2, NAT_1:11, XREAL_1:9;
F3:
k2 + 1
in dom ((B * A2) * C)
by E5b, K11, FINSEQ_3:27;
K4:
[k2,j] in Indices F
by F2, E1, MATRIX_1:38;
K5:
[k2,(j0 -' 1)] in Indices F
by K4, NAT_D:34;
F30:
((B * A2) * C) * (k2 + 1),
((j0 -' 1) + 1) = F * k2,
(j0 -' 1)
by D12, K5;
K6:
k2 in Seg k
by E5, E46, F0, F33, FINSEQ_1:def 3;
K7:
k2 in dom F
by E5, K6, FINSEQ_1:def 3;
((B * A2) * C) * (k2 + 1),
((j0 -' 1) + 1) = (Col F,(j0 -' 1)) . k2
by F30, K7, MATRIX_1:def 9;
hence
(Col ((B * A2) * C),(j + 1)) . ((len <*(0. K)*>) + k2) = (Col F,j) . k2
by F33, E22, F3, MATRIX_1:def 9;
:: thesis: verum
end;
then E19:
<*(0. K)*> ^ (Col F,j) = Col ((B * A2) * C),
(j + 1)
by E30b, E31b, FINSEQ_1:def 7;
E20:
len (Line G,i) =
width G
by MATRIX_1:def 8
.=
k
by MATRIX_1:25
;
E21:
len (Col F,j) =
len F
by MATRIX_1:def 9
.=
k
by MATRIX_1:25
;
E23:
((((C ~ ) * B2) * (B ~ )) * ((B * A2) * C)) * (i + 1),
(j + 1) =
|((Line (((C ~ ) * B2) * (B ~ )),(i + 1)),(Col ((B * A2) * C),(j + 1)))|
by E3b, E4b, E5b, MATRIX_3:def 4
.=
|(<*(0. K)*>,<*(0. K)*>)| + |((Line G,i),(Col F,j))|
by BB250, E20, E21, E18, E19, E22
.=
(0. K) + |((Line G,i),(Col F,j))|
by BB270
.=
|((Line G,i),(Col F,j))|
by RLVECT_1:10
;
now per cases
( i = j or i <> j )
;
suppose F0:
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 E12, E13, E13a, MATRIX_1:38;
then
(1. K,(k + 1)) * (i + 1),
(j + 1) = 1. K
by F0, MATRIX_1:def 12;
hence
(1. K,(k + 1)) * (i + 1),
(j + 1) = IFEQ i,
j,
(1. K),
(0. K)
by F0, FUNCOP_1:def 8;
:: thesis: verum end; suppose F0:
i <> j
;
:: thesis: (1. K,(k + 1)) * (i + 1),(j + 1) = IFEQ i,j,(1. K),(0. K)F3:
[(i + 1),(j + 1)] in Indices (1. K,(k + 1))
by E12, E13, E13a, MATRIX_1:38;
(
i + 1
<> j + 1 implies
(1. K,(k + 1)) * (i + 1),
(j + 1) = 0. K )
by F3, MATRIX_1:def 12;
hence
(1. K,(k + 1)) * (i + 1),
(j + 1) = IFEQ i,
j,
(1. K),
(0. K)
by F0, FUNCOP_1:def 8;
:: thesis: verum end;
hence
(G * F) * i,
j = IFEQ i,
j,
(1. K),
(0. K)
by E23, E3, E4, E5, D44, MATRIX_3:def 4;
:: thesis: verum
end;
then
G * F = 1. K,
k
by BB370;
then consider G2 being
Matrix of
k,
K such that D16:
F * G2 = 1. K,
k
by C1;
D16b:
(
len F = k &
width F = k &
Indices F = [:(Seg k),(Seg k):] )
by MATRIX_1:25;
D16c:
(
len G2 = k &
width G2 = k &
Indices G2 = [:(Seg k),(Seg k):] )
by MATRIX_1:25;
deffunc H3(
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)));
consider B4 being
Matrix of
k + 1,
k + 1,
K such that D13:
for
i,
j being
Nat st
[i,j] in Indices B4 holds
B4 * i,
j = H3(
i,
j)
from MATRIX_1:sch 1();
D70:
(
len B4 = k + 1 &
width B4 = k + 1 &
Indices B4 = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
D71:
(
len (((B * A2) * C) * B4) = k + 1 &
width (((B * A2) * C) * B4) = k + 1 &
Indices (((B * A2) * C) * B4) = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
D92c:
len (Line ((B * A2) * C),1) =
width ((B * A2) * C)
by MATRIX_1:def 8
.=
k + 1
by MATRIX_1:25
;
D92k:
len (Line ((B * A2) * C),1) = len (Base_FinSeq K,(k + 1),1)
by AA1100, D92c;
D94a:
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 E0:
( 1
<= j &
j <= len (Line ((B * A2) * C),1) )
;
:: thesis: (Line ((B * A2) * C),1) . j = (Base_FinSeq K,(k + 1),1) . j
E1:
len (Line ((B * A2) * C),1) = width ((B * A2) * C)
by MATRIX_1:def 8;
E2:
j in Seg (width ((B * A2) * C))
by E0, E1, FINSEQ_1:3;
E3:
( 1
<= j &
j <= k + 1 )
by E0, E5b, MATRIX_1:def 8;
E3b:
1
<= k + 1
by E3, XXREAL_0:2;
per cases
( 1 = j or 1 < j )
by E0, XXREAL_0:1;
suppose F0:
1
< j
;
:: thesis: (Line ((B * A2) * C),1) . j = (Base_FinSeq K,(k + 1),1) . jB:
j in NAT
by ORDINAL1:def 13;
(Line ((B * A2) * C),1) . j =
((B * A2) * C) * 1,
j
by E2, MATRIX_1:def 8
.=
0. K
by D9, F0, E3, B
;
hence
(Line ((B * A2) * C),1) . j = (Base_FinSeq K,(k + 1),1) . j
by AA1120, E3, F0, E3b;
:: thesis: verum end;
end;
D94:
Line ((B * A2) * C),1
= Base_FinSeq K,
(k + 1),1
by D92k, D94a, FINSEQ_1:18;
len (Col B4,1) =
len B4
by MATRIX_1:def 9
.=
k + 1
by MATRIX_1:25
;
then D92:
len (Col B4,1) = len (Base_FinSeq K,(k + 1),1)
by AA1100;
D95a:
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 E0:
( 1
<= j &
j <= len (Col B4,1) )
;
:: thesis: (Col B4,1) . j = (Base_FinSeq K,(k + 1),1) . j
E1:
len (Col B4,1) = len B4
by MATRIX_1:def 9;
E1b:
j in Seg (width B4)
by E0, D70, E1, FINSEQ_1:3;
E2:
j in dom B4
by D70, E1b, FINSEQ_1:def 3;
E3:
( 1
<= j &
j <= k + 1 )
by E0, D70, MATRIX_1:def 9;
E3b:
1
<= k + 1
by E3, XXREAL_0:2;
F2:
[j,1] in Indices B4
by E3, E3b, MATRIX_1:38;
per cases
( 1 = j or 1 < j )
by E0, XXREAL_0:1;
suppose F0:
1
= j
;
:: thesis: (Col B4,1) . j = (Base_FinSeq K,(k + 1),1) . j(Col B4,1) . j =
B4 * j,1
by E2, 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 D13, F2
.=
IFEQ 1,1,
(1. K),
(0. K)
by F0, FUNCOP_1:def 8
.=
1. K
by FUNCOP_1:def 8
;
hence
(Col B4,1) . j = (Base_FinSeq K,(k + 1),1) . j
by F0, AA1110, E3;
:: thesis: verum end; suppose F0:
1
< j
;
:: thesis: (Col B4,1) . j = (Base_FinSeq K,(k + 1),1) . j(Col B4,1) . j =
B4 * j,1
by E2, 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 D13, F2
.=
IFEQ 1,1,
(0. K),
(G2 * (j -' 1),(1 -' 1))
by F0, FUNCOP_1:def 8
.=
0. K
by FUNCOP_1:def 8
;
hence
(Col B4,1) . j = (Base_FinSeq K,(k + 1),1) . j
by AA1120, E3, F0, E3b;
:: thesis: verum end;
end;
D95:
Col B4,1
= Base_FinSeq K,
(k + 1),1
by D92, D95a, FINSEQ_1:18;
D100:
1
<= k + 1
by NAT_1:11;
FF0:
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 )
assume E0:
[i,j] in Indices (((B * A2) * C) * B4)
;
:: thesis: (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j
reconsider i0 =
i,
j0 =
j as
Element of
NAT by ORDINAL1:def 13;
E20b:
len (Line F,(i -' 1)) =
width F
by MATRIX_1:def 8
.=
k
by MATRIX_1:25
;
E21b:
len (Col G2,(j -' 1)) =
len G2
by MATRIX_1:def 9
.=
k
by MATRIX_1:25
;
E40c:
len (Line ((B * A2) * C),i) =
width ((B * A2) * C)
by MATRIX_1:def 8
.=
k + 1
by MATRIX_1:25
;
E40d:
len (Col B4,j) =
len B4
by MATRIX_1:def 9
.=
k + 1
by MATRIX_1:25
;
E103:
(
i in Seg (k + 1) &
j in Seg (k + 1) )
by E0, D71, ZFMISC_1:106;
E3:
( 1
<= i &
i <= k + 1 & 1
<= j &
j <= k + 1 )
by E103, FINSEQ_1:3;
E4b:
(
len B4 = k + 1 &
width B4 = k + 1 &
Indices B4 = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
E4c:
(
len ((B * A2) * C) = k + 1 &
width ((B * A2) * C) = k + 1 &
Indices ((B * A2) * C) = [:(Seg (k + 1)),(Seg (k + 1)):] )
by MATRIX_1:25;
E89:
[i,j] in Indices B4
by D71, E0, MATRIX_1:25;
E101:
[i,j] in [:(Seg (k + 1)),(Seg (k + 1)):]
by E0, MATRIX_1:25;
E104:
[i,j] in Indices (1. K,(k + 1))
by E101, MATRIX_1:25;
now per cases
( i = 1 or 1 < i )
by E3, XXREAL_0:1;
suppose F0:
i = 1
;
:: thesis: (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,jnow per cases
( j = 1 or j > 1 )
by E3, XXREAL_0:1;
suppose G0:
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 E0, E4b, E4c, MATRIX_3:def 4
.=
1. K
by D94, AA2629, D95, D100, F0, G0
;
hence
(((B * A2) * C) * B4) * i,
j = (1. K,(k + 1)) * i,
j
by F0, G0, E104, MATRIX_1:def 12;
:: thesis: verum end; suppose G0:
j > 1
;
:: thesis: (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j
1
<= len B4
by D100, MATRIX_1:25;
then G5:
1
in dom B4
by FINSEQ_3:27;
(((B * A2) * C) * B4) * i,
j =
|((Line ((B * A2) * C),i0),(Col B4,j0))|
by E0, E4b, E4c, MATRIX_3:def 4
.=
|((Base_FinSeq K,(k + 1),1),(Col B4,j0))|
by F0, D92k, D94a, FINSEQ_1:18
.=
|((Col B4,j0),(Base_FinSeq K,(k + 1),1))|
by FVSUM_1:115
.=
(Col B4,j0) . 1
by AA2627, E40d, D100
.=
B4 * 1,
j
by G5, 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 D13, E89, F0
.=
IFEQ j,1,
(1. K),
(0. K)
by F0, FUNCOP_1:def 8
.=
0. K
by G0, FUNCOP_1:def 8
;
hence
(((B * A2) * C) * B4) * i,
j = (1. K,(k + 1)) * i,
j
by F0, G0, E30, E101, MATRIX_1:def 12;
:: thesis: verum hence
(((B * A2) * C) * B4) * i,
j = (1. K,(k + 1)) * i,
j
;
:: thesis: verum suppose F0:
1
< i
;
:: thesis: (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,jthen F1b:
1
+ 1
<= i
by NAT_1:13;
now per cases
( j = 1 or j > 1 )
by E3, XXREAL_0:1;
suppose H0:
j = 1
;
:: thesis: (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,jH5:
len (Line ((B * A2) * C),i) =
width ((B * A2) * C)
by MATRIX_1:def 8
.=
k + 1
by MATRIX_1:25
;
H6:
1
in Seg (width ((B * A2) * C))
by E5b, D100, FINSEQ_1:3;
(((B * A2) * C) * B4) * i,
j =
|((Line ((B * A2) * C),i0),(Col B4,j0))|
by E0, E4b, E4c, MATRIX_3:def 4
.=
|((Line ((B * A2) * C),i),(Base_FinSeq K,(k + 1),1))|
by D92, D95a, H0, FINSEQ_1:18
.=
(Line ((B * A2) * C),i) . 1
by AA2627, H5, D100
.=
((B * A2) * C) * i0,1
by H6, MATRIX_1:def 8
.=
0. K
by D9, F0, E3
;
hence
(((B * A2) * C) * B4) * i,
j = (1. K,(k + 1)) * i,
j
by F0, E104, H0, MATRIX_1:def 12;
:: thesis: verum end; suppose G0:
j > 1
;
:: thesis: (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,jG1b:
1
+ 1
<= j
by G0, NAT_1:13;
G1:
i -' 1
= i - 1
by F0, XREAL_1:235;
G2:
1
<= i - 1
by F1b, XREAL_1:21;
G3:
j -' 1
= j - 1
by G0, XREAL_1:235;
G4:
1
<= j - 1
by G1b, XREAL_1:21;
G5:
i -' 1
<= k
by E3, G1, XREAL_1:22;
G6:
j -' 1
<= k
by E3, G3, XREAL_1:22;
G7:
i -' 1
in Seg k
by G1, G2, G5, FINSEQ_1:3;
j -' 1
in Seg k
by G3, G4, G6, FINSEQ_1:3;
then G9:
[(i -' 1),(j -' 1)] in [:(Seg k),(Seg k):]
by G7, ZFMISC_1:106;
E45b:
len (Line F,(i -' 1)) =
width F
by MATRIX_1:def 8
.=
k
by MATRIX_1:25
;
E46:
len (Col G2,(j -' 1)) =
len G2
by MATRIX_1:def 9
.=
k
by MATRIX_1:25
;
E30a:
dom (Line ((B * A2) * C),((i -' 1) + 1)) =
Seg (k + 1)
by E40c, G1, FINSEQ_1:def 3
.=
Seg ((len <*(0. K)*>) + (len (Line F,(i -' 1))))
by E45b, FINSEQ_1:56
;
E31:
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 F1a:
k2 in dom <*(0. K)*>
;
:: thesis: (Line ((B * A2) * C),((i -' 1) + 1)) . k2 = <*(0. K)*> . k2
F1b:
k2 in Seg (len <*(0. K)*>)
by F1a, FINSEQ_1:def 3;
F1d:
k2 in {1}
by F1b, FINSEQ_1:4, FINSEQ_1:57;
F5:
k2 = 1
by F1d, TARSKI:def 1;
F1e:
1
<= k + 1
by NAT_1:11;
F12:
k2 in Seg (width ((B * A2) * C))
by E4c, F5, F1e, FINSEQ_1:3;
F1g:
((B * A2) * C) * i0,1
= 0. K
by D9, E3, F0;
(Line ((B * A2) * C),i) . k2 = 0. K
by F12, F5, F1g, MATRIX_1:def 8;
hence
(Line ((B * A2) * C),((i -' 1) + 1)) . k2 = <*(0. K)*> . k2
by G1, F5, FINSEQ_1:57;
:: thesis: verum
end;
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 F2a:
k2 in dom (Line F,(i -' 1))
;
:: thesis: (Line ((B * A2) * C),((i -' 1) + 1)) . ((len <*(0. K)*>) + k2) = (Line F,(i -' 1)) . k2
F2b:
k2 in Seg (len (Line F,(i -' 1)))
by F2a, FINSEQ_1:def 3;
F2:
( 1
<= k2 &
k2 <= k )
by E45b, F2b, FINSEQ_1:3;
F2d:
( 1
<= k2 + 1 &
k2 + 1
<= k + 1 )
by F2, NAT_1:11, XREAL_1:9;
F3:
k2 + 1
in Seg (width ((B * A2) * C))
by E4c, F2d, FINSEQ_1:3;
F2f:
[(i -' 1),k2] in Indices F
by F2, G1, G2, G5, MATRIX_1:38;
F30:
((B * A2) * C) * ((i -' 1) + 1),
(k2 + 1) = F * (i -' 1),
k2
by D12, F2f;
F2h:
k2 in Seg (width F)
by D16b, E45b, F2a, FINSEQ_1:def 3;
F2k:
((B * A2) * C) * ((i -' 1) + 1),
(k2 + 1) = (Line F,(i -' 1)) . k2
by F30, F2h, MATRIX_1:def 8;
(Line ((B * A2) * C),((i -' 1) + 1)) . (k2 + 1) = (Line F,(i -' 1)) . k2
by F3, F2k, 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: verum
end; then E18:
<*(0. K)*> ^ (Line F,(i -' 1)) = Line ((B * A2) * C),
((i -' 1) + 1)
by E30a, E31, FINSEQ_1:def 7;
E30b:
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 E46, E40d, G3, FINSEQ_1:56
;
E31b:
for
k2 being
Nat st
k2 in dom <*(0. K)*> holds
(Col B4,((j -' 1) + 1)) . k2 = <*(0. K)*> . k2
proof
let k2 be
Nat;
:: thesis: ( k2 in dom <*(0. K)*> implies (Col B4,((j -' 1) + 1)) . k2 = <*(0. K)*> . k2 )
assume F8a:
k2 in dom <*(0. K)*>
;
:: thesis: (Col B4,((j -' 1) + 1)) . k2 = <*(0. K)*> . k2
F8b:
k2 in Seg (len <*(0. K)*>)
by F8a, FINSEQ_1:def 3;
F8d:
k2 in {1}
by F8b, FINSEQ_1:4, FINSEQ_1:57;
F5:
k2 = 1
by F8d, TARSKI:def 1;
F8e:
1
<= 1
+ k
by NAT_1:11;
F8f:
1
<= k + 1
by NAT_1:11;
F8g:
k2 in Seg (len B4)
by F5, E4b, F8f, FINSEQ_1:3;
F12:
k2 in dom B4
by F8g, FINSEQ_1:def 3;
F8h:
[1,j] in Indices B4
by F8e, E3, MATRIX_1:38;
F8k:
B4 * 1,
j = IFEQ 1,1,
(IFEQ j,1,(1. K),(0. K)),
(IFEQ j,1,(0. K),(G2 * (1 -' 1),(j -' 1)))
by D13, F8h;
F8m:
B4 * 1,
j =
IFEQ j,1,
(1. K),
(0. K)
by F8k, FUNCOP_1:def 8
.=
0. K
by G0, FUNCOP_1:def 8
;
(Col B4,j) . k2 = 0. K
by F12, F5, F8m, MATRIX_1:def 9;
hence
(Col B4,((j -' 1) + 1)) . k2 = <*(0. K)*> . k2
by G3, F5, FINSEQ_1:57;
:: thesis: verum
end;
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 F3a:
k2 in dom (Col G2,(j -' 1))
;
:: thesis: (Col B4,((j -' 1) + 1)) . ((len <*(0. K)*>) + k2) = (Col G2,(j -' 1)) . k2
F2:
( 1
<= k2 &
k2 <= k )
by E46, F3a, FINSEQ_3:27;
F20:
1
< k2 + 1
by F2, NAT_1:13;
F3e:
( 1
<= k2 + 1 &
k2 + 1
<= k + 1 )
by F2, NAT_1:11, XREAL_1:9;
F3:
k2 + 1
in dom B4
by E4b, F3e, FINSEQ_3:27;
F3g:
[(k2 + 1),j] in Indices B4
by F3e, E3, MATRIX_1:38;
F3h:
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 D13, F3g;
F30:
B4 * (k2 + 1),
j =
IFEQ j,1,
(0. K),
(G2 * ((k2 + 1) -' 1),(j -' 1))
by F20, F3h, FUNCOP_1:def 8
.=
G2 * ((k2 + 1) -' 1),
(j -' 1)
by G0, FUNCOP_1:def 8
.=
G2 * k2,
(j -' 1)
by NAT_D:34
;
F3k:
k2 in Seg k
by E46, F3a, FINSEQ_1:def 3;
F10:
k2 in dom G2
by D16c, F3k, FINSEQ_1:def 3;
F3m:
B4 * (k2 + 1),
((j -' 1) + 1) = (Col G2,(j -' 1)) . k2
by F30, F10, G3, MATRIX_1:def 9;
(Col B4,((j -' 1) + 1)) . (k2 + 1) = (Col G2,(j -' 1)) . k2
by F3, F3m, MATRIX_1:def 9;
hence
(Col B4,((j -' 1) + 1)) . ((len <*(0. K)*>) + k2) = (Col G2,(j -' 1)) . k2
by FINSEQ_1:57;
:: thesis: verum
end; then E19:
<*(0. K)*> ^ (Col G2,(j -' 1)) = Col B4,
((j -' 1) + 1)
by E30b, E31b, FINSEQ_1:def 7;
E88c:
[(i -' 1),(j -' 1)] in Indices (F * G2)
by G9, MATRIX_1:25;
E88b:
[(i -' 1),(j -' 1)] in Indices (1. K,k)
by G9, MATRIX_1:25;
E160:
(i -' 1) + 1 =
(i - 1) + 1
by F0, XREAL_1:235
.=
i
;
E161:
(j -' 1) + 1 =
(j - 1) + 1
by G0, XREAL_1:235
.=
j
;
G4:
(((B * A2) * C) * B4) * i,
j =
|((Line ((B * A2) * C),((i -' 1) + 1)),(Col B4,((j -' 1) + 1)))|
by E160, E161, E0, E4b, E4c, MATRIX_3:def 4
.=
|(<*(0. K)*>,<*(0. K)*>)| + |((Line F,(i -' 1)),(Col G2,(j -' 1)))|
by BB250, E20b, E21b, E18, E19, E22
.=
(0. K) + |((Line F,(i -' 1)),(Col G2,(j -' 1)))|
by BB270
.=
(0. K) + ((F * G2) * (i -' 1),(j -' 1))
by E88c, D16b, D16c, MATRIX_3:def 4
.=
(1. K,k) * (i -' 1),
(j -' 1)
by D16, RLVECT_1:10
;
now per cases
( i = j or i <> j )
;
suppose H0:
i <> j
;
:: thesis: (((B * A2) * C) * B4) * i,j = (1. K,(k + 1)) * i,j
i - 1
<> j - 1
by H0;
then
i0 -' 1
<> j0 -' 1
by F0, G3, XREAL_1:235;
then
(1. K,k) * (i0 -' 1),
(j0 -' 1) = 0. K
by E88b, MATRIX_1:def 12;
hence
(((B * A2) * C) * B4) * i,
j = (1. K,(k + 1)) * i,
j
by E104, H0, G4, MATRIX_1:def 12;
:: thesis: verum end; hence
(((B * A2) * C) * B4) * i,
j = (1. K,(k + 1)) * i,
j
;
:: thesis: verum end; hence
(((B * A2) * C) * B4) * i,
j = (1. K,(k + 1)) * i,
j
;
:: thesis: verum end;
hence
(((B * A2) * C) * B4) * i,
j = (1. K,(k + 1)) * i,
j
;
:: thesis: verum
end;
K2:
width (Inv B) = k + 1
by MATRIX_1:25;
K3:
len (A2 * (C * B4)) = k + 1
by MATRIX_1:25;
K3a:
((B * A2) * C) * B4 = 1. K,
(k + 1)
by FF0, MATRIX_1:28;
K3b:
(Inv B) * (((B * A2) * C) * B4) = Inv B
by K2, K3a, MATRIXR2:67;
K3c:
((Inv B) * (((B * A2) * C) * B4)) * B = 1. K,
(k + 1)
by D9, AA4140, K3b;
K3d:
((Inv B) * ((B * A2) * (C * B4))) * B = 1. K,
(k + 1)
by AA41, K3c;
K3e:
((Inv B) * (B * (A2 * (C * B4)))) * B = 1. K,
(k + 1)
by AA41, K3d;
K3f:
(((Inv B) * B) * (A2 * (C * B4))) * B = 1. K,
(k + 1)
by AA41, K3e;
K3g:
((1. K,(k + 1)) * (A2 * (C * B4))) * B = 1. K,
(k + 1)
by D9, AA4140, K3f;
K3h:
(A2 * (C * B4)) * B = 1. K,
(k + 1)
by K3, K3g, MATRIXR2:68;
A2 * ((C * B4) * B) = 1. K,
(k + 1)
by AA41, K3h;
hence
ex
B4 being
Matrix of
k + 1,
K st
A2 * B4 = 1. K,
(k + 1)
;
:: thesis: verum
end;
hence
S1[
k + 1]
;
:: thesis: verum
end;
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(B3, B4);
hence
ex
B2 being
Matrix of
n,
K st
A * B2 = 1. K,
n
by B1;
:: thesis: verum
end;