let i1, i2, j be Nat; :: thesis: 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); :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum