let j, i1, i2 be Element of NAT ; for G being Matrix of (TOP-REAL 2) st G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds
(G * i1,j) `1 < (G * i2,j) `1
let G be Matrix of (TOP-REAL 2); ( G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i1 & i1 < i2 & i2 <= len G implies (G * i1,j) `1 < (G * i2,j) `1 )
assume that
A1:
G is X_increasing-in-column
and
A2:
1 <= j
and
A3:
j <= width G
and
A4:
1 <= i1
and
A5:
i1 < i2
and
A6:
i2 <= len G
; (G * i1,j) `1 < (G * i2,j) `1
j in Seg (width G)
by A2, A3, FINSEQ_1:3;
then A7:
X_axis (Col G,j) is increasing
by A1, GOBOARD1:def 9;
reconsider c = Col G,j as FinSequence of (TOP-REAL 2) ;
A8:
i1 <= len G
by A5, A6, XXREAL_0:2;
then A9:
i1 in dom G
by A4, FINSEQ_3:27;
A10:
1 <= i2
by A4, A5, XXREAL_0:2;
then A11:
i2 in dom G
by A6, FINSEQ_3:27;
A12:
len c = len G
by MATRIX_1:def 9;
then
i1 in dom c
by A4, A8, FINSEQ_3:27;
then A13:
c /. i1 = c . i1
by PARTFUN1:def 8;
i2 in dom c
by A6, A10, A12, FINSEQ_3:27;
then A14:
c /. i2 = c . i2
by PARTFUN1:def 8;
A15:
len (X_axis (Col G,j)) = len c
by GOBOARD1:def 3;
then A16:
i1 in dom (X_axis (Col G,j))
by A4, A8, A12, FINSEQ_3:27;
A17: (G * i1,j) `1 =
(c /. i1) `1
by A9, A13, MATRIX_1:def 9
.=
(X_axis (Col G,j)) . i1
by A16, GOBOARD1:def 3
;
A18:
i2 in dom (X_axis (Col G,j))
by A6, A10, A12, A15, FINSEQ_3:27;
then (X_axis (Col G,j)) . i2 =
(c /. i2) `1
by GOBOARD1:def 3
.=
(G * i2,j) `1
by A11, A14, MATRIX_1:def 9
;
hence
(G * i1,j) `1 < (G * i2,j) `1
by A5, A7, A16, A17, A18, SEQM_3:def 1; verum