let S1, S2 be Matrix of n,m,D; ( ( for i, j being Nat st [i,j] in Indices S1 holds
S1 * (i,j) = M * ((nt . i),(mt . j)) ) & ( for i, j being Nat st [i,j] in Indices S2 holds
S2 * (i,j) = M * ((nt . i),(mt . j)) ) implies S1 = S2 )
assume that
A2:
for i, j being Nat st [i,j] in Indices S1 holds
S1 * (i,j) = M * ((nt . i),(mt . j))
and
A3:
for i, j being Nat st [i,j] in Indices S2 holds
S2 * (i,j) = M * ((nt . i),(mt . j))
; S1 = S2
now for i, j being Nat st [i,j] in Indices S1 holds
S1 * (i,j) = S2 * (i,j)let i,
j be
Nat;
( [i,j] in Indices S1 implies S1 * (i,j) = S2 * (i,j) )assume A4:
[i,j] in Indices S1
;
S1 * (i,j) = S2 * (i,j)A5:
[i,j] in Indices S2
by A4, MATRIX_0:26;
reconsider i9 =
i,
j9 =
j as
Element of
NAT by ORDINAL1:def 12;
S1 * (
i,
j)
= M * (
(nt . i9),
(mt . j9))
by A2, A4;
hence
S1 * (
i,
j)
= S2 * (
i,
j)
by A3, A5;
verum end;
hence
S1 = S2
by MATRIX_0:27; verum