let i1, i2, j be 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:1;
then A7:
X_axis (Col (G,j)) is increasing
by A1;
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:25;
A10:
1 <= i2
by A4, A5, XXREAL_0:2;
then A11:
i2 in dom G
by A6, FINSEQ_3:25;
A12:
len c = len G
by MATRIX_0:def 8;
then
i1 in dom c
by A4, A8, FINSEQ_3:25;
then A13:
c /. i1 = c . i1
by PARTFUN1:def 6;
i2 in dom c
by A6, A10, A12, FINSEQ_3:25;
then A14:
c /. i2 = c . i2
by PARTFUN1:def 6;
A15:
len (X_axis (Col (G,j))) = len c
by GOBOARD1:def 1;
then A16:
i1 in dom (X_axis (Col (G,j)))
by A4, A8, A12, FINSEQ_3:25;
A17: (G * (i1,j)) `1 =
(c /. i1) `1
by A9, A13, MATRIX_0:def 8
.=
(X_axis (Col (G,j))) . i1
by A16, GOBOARD1:def 1
;
A18:
i2 in dom (X_axis (Col (G,j)))
by A6, A10, A12, A15, FINSEQ_3:25;
then (X_axis (Col (G,j))) . i2 =
(c /. i2) `1
by GOBOARD1:def 1
.=
(G * (i2,j)) `1
by A11, A14, MATRIX_0:def 8
;
hence
(G * (i1,j)) `1 < (G * (i2,j)) `1
by A5, A7, A16, A17, A18; verum