set M = Gauge C,n;
A1: len (Gauge C,n) = (2 |^ n) + 3 by Def1;
len (Gauge C,n) = width (Gauge C,n) by Def1;
hence not Gauge C,n is empty-yielding by A1, GOBOARD1:def 5; :: thesis: ( Gauge C,n is X_equal-in-line & Gauge C,n is Y_equal-in-column )
A2: Indices (Gauge C,n) = [:(dom (Gauge C,n)),(Seg (width (Gauge C,n))):] by MATRIX_1:def 5;
thus Gauge C,n is X_equal-in-line :: thesis: Gauge C,n is Y_equal-in-column

proof

let i be Element of NAT ; :: according to GOBOARD1:def 6 :: thesis: ( not i in dom (Gauge C,n) or X_axis (Line (Gauge C,n),i) is constant )
assume A3: i in dom (Gauge C,n) ; :: thesis: X_axis (Line (Gauge C,n),i) is constant
set l = Line (Gauge C,n),i;
set f = X_axis (Line (Gauge C,n),i);
let j1 be Element of NAT ; :: according to SEQM_3:def 15 :: thesis: for b₁ being Element of NAT holds
( not j1 in dom (X_axis (Line (Gauge C,n),i)) or not b₁ in dom (X_axis (Line (Gauge C,n),i)) or (X_axis (Line (Gauge C,n),i)) . j1 = (X_axis (Line (Gauge C,n),i)) . b₁ )
let j2 be Element of NAT ; :: thesis: ( not j1 in dom (X_axis (Line (Gauge C,n),i)) or not j2 in dom (X_axis (Line (Gauge C,n),i)) or (X_axis (Line (Gauge C,n),i)) . j1 = (X_axis (Line (Gauge C,n),i)) . j2 )
assume that
A4: j1 in dom (X_axis (Line (Gauge C,n),i)) and
A5: j2 in dom (X_axis (Line (Gauge C,n),i)) ; :: thesis: (X_axis (Line (Gauge C,n),i)) . j1 = (X_axis (Line (Gauge C,n),i)) . j2
len (Line (Gauge C,n),i) = width (Gauge C,n) by MATRIX_1:def 8;
then A6: dom (Line (Gauge C,n),i) = Seg (width (Gauge C,n)) by FINSEQ_1:def 3;
A7: dom (X_axis (Line (Gauge C,n),i)) = dom (Line (Gauge C,n),i) by SPRECT_2:19;
then A8: (Line (Gauge C,n),i) /. j1 = (Line (Gauge C,n),i) . j1 by A4, PARTFUN1:def 8
.= (Gauge C,n) * i,j1 by A4, A6, A7, MATRIX_1:def 8 ;
A9: [i,j1] in Indices (Gauge C,n) by A2, A3, A4, A6, A7, ZFMISC_1:106;
A10: (Line (Gauge C,n),i) /. j2 = (Line (Gauge C,n),i) . j2 by A5, A7, PARTFUN1:def 8
.= (Gauge C,n) * i,j2 by A5, A6, A7, MATRIX_1:def 8 ;
A11: [i,j2] in Indices (Gauge C,n) by A2, A3, A5, A6, A7, ZFMISC_1:106;
set x = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2));
set d = ((N-bound C) - (S-bound C)) / (2 |^ n);
thus (X_axis (Line (Gauge C,n),i)) . j1 = ((Line (Gauge C,n),i) /. j1) `1 by A4, GOBOARD1:def 3
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j1 - 2)))]| `1 by A8, A9, Def1
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2)) by EUCLID:56
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j2 - 2)))]| `1 by EUCLID:56
.= ((Line (Gauge C,n),i) /. j2) `1 by A10, A11, Def1
.= (X_axis (Line (Gauge C,n),i)) . j2 by A5, GOBOARD1:def 3 ; :: thesis: verum

end;

thus Gauge C,n is Y_equal-in-column :: thesis: verum

proof

let j be Element of NAT ; :: according to GOBOARD1:def 7 :: thesis: ( not j in Seg (width (Gauge C,n)) or Y_axis (Col (Gauge C,n),j) is constant )
assume A12: j in Seg (width (Gauge C,n)) ; :: thesis: Y_axis (Col (Gauge C,n),j) is constant
set c = Col (Gauge C,n),j;
set f = Y_axis (Col (Gauge C,n),j);
let i1 be Element of NAT ; :: according to SEQM_3:def 15 :: thesis: for b₁ being Element of NAT holds
( not i1 in dom (Y_axis (Col (Gauge C,n),j)) or not b₁ in dom (Y_axis (Col (Gauge C,n),j)) or (Y_axis (Col (Gauge C,n),j)) . i1 = (Y_axis (Col (Gauge C,n),j)) . b₁ )
let i2 be Element of NAT ; :: thesis: ( not i1 in dom (Y_axis (Col (Gauge C,n),j)) or not i2 in dom (Y_axis (Col (Gauge C,n),j)) or (Y_axis (Col (Gauge C,n),j)) . i1 = (Y_axis (Col (Gauge C,n),j)) . i2 )
assume that
A13: i1 in dom (Y_axis (Col (Gauge C,n),j)) and
A14: i2 in dom (Y_axis (Col (Gauge C,n),j)) ; :: thesis: (Y_axis (Col (Gauge C,n),j)) . i1 = (Y_axis (Col (Gauge C,n),j)) . i2
len (Col (Gauge C,n),j) = len (Gauge C,n) by MATRIX_1:def 9;
then A15: dom (Col (Gauge C,n),j) = dom (Gauge C,n) by FINSEQ_3:31;
A16: dom (Y_axis (Col (Gauge C,n),j)) = dom (Col (Gauge C,n),j) by SPRECT_2:20;
then A17: (Col (Gauge C,n),j) /. i1 = (Col (Gauge C,n),j) . i1 by A13, PARTFUN1:def 8
.= (Gauge C,n) * i1,j by A13, A15, A16, MATRIX_1:def 9 ;
A18: [i1,j] in Indices (Gauge C,n) by A2, A12, A13, A15, A16, ZFMISC_1:106;
A19: (Col (Gauge C,n),j) /. i2 = (Col (Gauge C,n),j) . i2 by A14, A16, PARTFUN1:def 8
.= (Gauge C,n) * i2,j by A14, A15, A16, MATRIX_1:def 9 ;
A20: [i2,j] in Indices (Gauge C,n) by A2, A12, A14, A15, A16, ZFMISC_1:106;
set y = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2));
set d = ((E-bound C) - (W-bound C)) / (2 |^ n);
thus (Y_axis (Col (Gauge C,n),j)) . i1 = ((Col (Gauge C,n),j) /. i1) `2 by A13, GOBOARD1:def 4
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `2 by A17, A18, Def1
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)) by EUCLID:56
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| `2 by EUCLID:56
.= ((Col (Gauge C,n),j) /. i2) `2 by A19, A20, Def1
.= (Y_axis (Col (Gauge C,n),j)) . i2 by A14, GOBOARD1:def 4 ; :: thesis: verum

end;