let M1, M2 be Matrix of n,K; :: thesis: ( ( for i being Nat st [i,i] in Indices M1 holds

M1 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M1 & i <> j holds

M1 * (i,j) = 0. K ) & ( for i being Nat st [i,i] in Indices M2 holds

M2 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M2 & i <> j holds

M2 * (i,j) = 0. K ) implies M1 = M2 )

assume that

A3: for i being Nat st [i,i] in Indices M1 holds

M1 * (i,i) = 1. K and

A4: for i, j being Nat st [i,j] in Indices M1 & i <> j holds

M1 * (i,j) = 0. K and

A5: for i being Nat st [i,i] in Indices M2 holds

M2 * (i,i) = 1. K and

A6: for i, j being Nat st [i,j] in Indices M2 & i <> j holds

M2 * (i,j) = 0. K ; :: thesis: M1 = M2

A7: Indices M1 = Indices M2 by MATRIX_0:26;

( len M1 = n & width M1 = n ) by MATRIX_0:24;

hence M1 = M2 by A8, A13, MATRIX_0:21; :: thesis: verum

M1 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M1 & i <> j holds

M1 * (i,j) = 0. K ) & ( for i being Nat st [i,i] in Indices M2 holds

M2 * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M2 & i <> j holds

M2 * (i,j) = 0. K ) implies M1 = M2 )

assume that

A3: for i being Nat st [i,i] in Indices M1 holds

M1 * (i,i) = 1. K and

A4: for i, j being Nat st [i,j] in Indices M1 & i <> j holds

M1 * (i,j) = 0. K and

A5: for i being Nat st [i,i] in Indices M2 holds

M2 * (i,i) = 1. K and

A6: for i, j being Nat st [i,j] in Indices M2 & i <> j holds

M2 * (i,j) = 0. K ; :: thesis: M1 = M2

A7: Indices M1 = Indices M2 by MATRIX_0:26;

A8: now :: thesis: for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = M2 * (i,j)

A13:
( len M2 = n & width M2 = n )
by MATRIX_0:24;M1 * (i,j) = M2 * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )

assume A9: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)

end;assume A9: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)

A10: now :: thesis: ( i <> j implies M1 * (i,j) = M2 * (i,j) )

assume A11:
i <> j
; :: thesis: M1 * (i,j) = M2 * (i,j)

then M1 * (i,j) = 0. K by A4, A9;

hence M1 * (i,j) = M2 * (i,j) by A7, A6, A9, A11; :: thesis: verum

end;then M1 * (i,j) = 0. K by A4, A9;

hence M1 * (i,j) = M2 * (i,j) by A7, A6, A9, A11; :: thesis: verum

now :: thesis: ( i = j implies M1 * (i,j) = M2 * (i,j) )

hence
M1 * (i,j) = M2 * (i,j)
by A10; :: thesis: verumassume A12:
i = j
; :: thesis: M1 * (i,j) = M2 * (i,j)

then M1 * (i,j) = 1. K by A3, A9;

hence M1 * (i,j) = M2 * (i,j) by A7, A5, A9, A12; :: thesis: verum

end;then M1 * (i,j) = 1. K by A3, A9;

hence M1 * (i,j) = M2 * (i,j) by A7, A5, A9, A12; :: thesis: verum

( len M1 = n & width M1 = n ) by MATRIX_0:24;

hence M1 = M2 by A8, A13, MATRIX_0:21; :: thesis: verum