consider M being Matrix of (2 |^ n) + 3,(2 |^ n) + 3, the carrier of (TOP-REAL 2) such that
A1: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H₁(i,j) from MATRIX_0:sch 1();
take M ; :: thesis: ( len M = (2 |^ n) + 3 & len M = width M & ( for i, j being Nat st [i,j] in Indices M holds
M * (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)))]| ) )
thus len M = (2 |^ n) + 3 by MATRIX_0:def 2; :: thesis: ( len M = width M & ( for i, j being Nat st [i,j] in Indices M holds
M * (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)))]| ) )
hence len M = width M by MATRIX_0:23; :: thesis: for i, j being Nat st [i,j] in Indices M holds
M * (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)))]|
thus for i, j being Nat st [i,j] in Indices M holds
M * (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)))]| by A1; :: thesis: verum