let C1, C2 be Matrix of n,K; ( ( for i, j being Nat st [i,j] in Indices C1 holds
C1 * (i,j) = Cofactor (M,i,j) ) & ( for i, j being Nat st [i,j] in Indices C2 holds
C2 * (i,j) = Cofactor (M,i,j) ) implies C1 = C2 )
assume that
A1:
for i, j being Nat st [i,j] in Indices C1 holds
C1 * (i,j) = Cofactor (M,i,j)
and
A2:
for i, j being Nat st [i,j] in Indices C2 holds
C2 * (i,j) = Cofactor (M,i,j)
; C1 = C2
now for i, j being Nat st [i,j] in Indices C1 holds
C1 * (i,j) = C2 * (i,j)A3:
Indices C1 = Indices C2
by MATRIX_0:26;
let i,
j be
Nat;
( [i,j] in Indices C1 implies C1 * (i,j) = C2 * (i,j) )assume A4:
[i,j] in Indices C1
;
C1 * (i,j) = C2 * (i,j)reconsider i9 =
i,
j9 =
j as
Element of
NAT by ORDINAL1:def 12;
C1 * (
i,
j)
= Cofactor (
M,
i9,
j9)
by A1, A4;
hence
C1 * (
i,
j)
= C2 * (
i,
j)
by A2, A4, A3;
verum end;
hence
C1 = C2
by MATRIX_0:27; verum