let C1, C2 be Matrix of n,K; :: thesis: ( ( 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
A2:
for i, j being Nat st [i,j] in Indices C1 holds
C1 * i,j = Cofactor M,i,j
and
A3:
for i, j being Nat st [i,j] in Indices C2 holds
C2 * i,j = Cofactor M,i,j
; :: thesis: C1 = C2
now let i,
j be
Nat;
:: thesis: ( [i,j] in Indices C1 implies C1 * i,j = C2 * i,j )assume A4:
[i,j] in Indices C1
;
:: thesis: C1 * i,j = C2 * i,jreconsider i' =
i,
j' =
j as
Element of
NAT by ORDINAL1:def 13;
Indices C1 = Indices C2
by MATRIX_1:27;
then
(
C1 * i,
j = Cofactor M,
i',
j' &
C2 * i,
j = Cofactor M,
i',
j' )
by A2, A3, A4;
hence
C1 * i,
j = C2 * i,
j
;
:: thesis: verum end;
hence
C1 = C2
by MATRIX_1:28; :: thesis: verum