consider M being Matrix of (2 |^ n) + 3,(2 |^ n) + 3, the carrier of (TOP-REAL 2) such that
A2: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H₁(i,j) from MATRIX_1: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_1: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 A1, MATRIX_1: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 A2; :: thesis: verum