let R be non empty Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds [1,1] in Indices (Gauge R,n)
let n be Element of NAT ; :: thesis: [1,1] in Indices (Gauge R,n)
A1: len (Gauge R,n) = width (Gauge R,n) by JORDAN8:def 1;
1 <= len (Gauge R,n) by Lm3;
hence [1,1] in Indices (Gauge R,n) by A1, MATRIX_1:37; :: thesis: verum