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 Gauge (C,n) is V3() by A1, MATRIX_0:def 10; :: 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_0:def 4;
thus Gauge (C,n) is X_equal-in-line :: thesis: Gauge (C,n) is Y_equal-in-column
proof
let i be Nat; :: according to GOBOARD1:def 4 :: 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 Nat; :: according to SEQM_3:def 10 :: thesis: for b1 being set holds
( not j1 in dom (X_axis (Line ((Gauge (C,n)),i))) or not b1 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))) . b1 )
let j2 be 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_0:def 7;
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:15;
then A8: (Line ((Gauge (C,n)),i)) /. j1 = (Line ((Gauge (C,n)),i)) . j1 by A4, PARTFUN1:def 6
.= (Gauge (C,n)) * (i,j1) by A4, A6, A7, MATRIX_0:def 7 ;
A9: [i,j1] in Indices (Gauge (C,n)) by A2, A3, A4, A6, A7, ZFMISC_1:87;
A10: (Line ((Gauge (C,n)),i)) /. j2 = (Line ((Gauge (C,n)),i)) . j2 by A5, A7, PARTFUN1:def 6
.= (Gauge (C,n)) * (i,j2) by A5, A6, A7, MATRIX_0:def 7 ;
A11: [i,j2] in Indices (Gauge (C,n)) by A2, A3, A5, A6, A7, ZFMISC_1:87;
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 1
.= |[((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:52
.= |[((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:52
.= ((Line ((Gauge (C,n)),i)) /. j2) `1 by A10, A11, Def1
.= (X_axis (Line ((Gauge (C,n)),i))) . j2 by A5, GOBOARD1:def 1 ; :: thesis: verum
end;
thus Gauge (C,n) is Y_equal-in-column :: thesis: verum
proof
let j be Nat; :: according to GOBOARD1:def 5 :: 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 Nat; :: according to SEQM_3:def 10 :: thesis: for b1 being set holds
( not i1 in dom (Y_axis (Col ((Gauge (C,n)),j))) or not b1 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))) . b1 )
let i2 be 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_0:def 8;
then A15: dom (Col ((Gauge (C,n)),j)) = dom (Gauge (C,n)) by FINSEQ_3:29;
A16: dom (Y_axis (Col ((Gauge (C,n)),j))) = dom (Col ((Gauge (C,n)),j)) by SPRECT_2:16;
then A17: (Col ((Gauge (C,n)),j)) /. i1 = (Col ((Gauge (C,n)),j)) . i1 by A13, PARTFUN1:def 6
.= (Gauge (C,n)) * (i1,j) by A13, A15, A16, MATRIX_0:def 8 ;
A18: [i1,j] in Indices (Gauge (C,n)) by A2, A12, A13, A15, A16, ZFMISC_1:87;
A19: (Col ((Gauge (C,n)),j)) /. i2 = (Col ((Gauge (C,n)),j)) . i2 by A14, A16, PARTFUN1:def 6
.= (Gauge (C,n)) * (i2,j) by A14, A15, A16, MATRIX_0:def 8 ;
A20: [i2,j] in Indices (Gauge (C,n)) by A2, A12, A14, A15, A16, ZFMISC_1:87;
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 2
.= |[((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:52
.= |[((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:52
.= ((Col ((Gauge (C,n)),j)) /. i2) `2 by A19, A20, Def1
.= (Y_axis (Col ((Gauge (C,n)),j))) . i2 by A14, GOBOARD1:def 2 ; :: thesis: verum
end;