let M1, M2 be Matrix of (TOP-REAL 2); ( len M1 = (2 |^ n) + 3 & len M1 = width M1 & ( for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) & len M2 = (2 |^ n) + 3 & len M2 = width M2 & ( for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) implies M1 = M2 )
assume that
A2:
len M1 = (2 |^ n) + 3
and
A3:
len M1 = width M1
and
A4:
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H1(i,j)
and
A5:
len M2 = (2 |^ n) + 3
and
A6:
len M2 = width M2
and
A7:
for i, j being Nat st [i,j] in Indices M2 holds
M2 * (i,j) = H1(i,j)
; M1 = M2
now for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)let i,
j be
Nat;
( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )assume A8:
[i,j] in Indices M1
;
M1 * (i,j) = M2 * (i,j)A9:
M1 is
Matrix of
(2 |^ n) + 3,
(2 |^ n) + 3, the
carrier of
(TOP-REAL 2)
by A2, A3, MATRIX_0:20;
M2 is
Matrix of
(2 |^ n) + 3,
(2 |^ n) + 3, the
carrier of
(TOP-REAL 2)
by A5, A6, MATRIX_0:20;
then A10:
[i,j] in Indices M2
by A8, A9, MATRIX_0:26;
thus M1 * (
i,
j) =
H1(
i,
j)
by A4, A8
.=
M2 * (
i,
j)
by A7, A10
;
verum end;
hence
M1 = M2
by A2, A3, A5, A6, MATRIX_0:21; verum