set M = GoB v1,v2;
A1: ( rng v1 c= REAL & rng v2 c= REAL & dom v1 = Seg (len v1) & dom v2 = Seg (len v2) ) by FINSEQ_1:def 3, FINSEQ_1:def 4;
A2: ( len (GoB v1,v2) = len v1 & width (GoB v1,v2) = len v2 ) by Def1;
then A3: ( dom (GoB v1,v2) = dom v1 & width (GoB v1,v2) = len v2 ) by FINSEQ_3:31;
then A4: Indices (GoB v1,v2) = [:(dom v1),(Seg (len v2)):] by MATRIX_1:def 5;
thus GoB v1,v2 is Y_increasing-in-line :: thesis: GoB v1,v2 is X_increasing-in-column

proof

let n be Element of NAT ; :: according to GOBOARD1:def 8 :: thesis: ( not n in dom (GoB v1,v2) or Y_axis (Line (GoB v1,v2),n) is increasing )
reconsider l = Line (GoB v1,v2),n as FinSequence of (TOP-REAL 2) ;
set y = Y_axis l;
assume A5: n in dom (GoB v1,v2) ; :: thesis: Y_axis (Line (GoB v1,v2),n) is increasing
A6: ( len (Y_axis l) = len l & len l = width (GoB v1,v2) & dom (Y_axis l) = Seg (len (Y_axis l)) ) by FINSEQ_1:def 3, GOBOARD1:def 4, MATRIX_1:def 8;
then A7: dom (Y_axis l) = dom l by FINSEQ_3:31;

now

let i, j be Element of NAT ; :: thesis: ( i in dom (Y_axis l) & j in dom (Y_axis l) & i < j implies (Y_axis l) . i < (Y_axis l) . j )
assume A8: ( i in dom (Y_axis l) & j in dom (Y_axis l) & i < j ) ; :: thesis: (Y_axis l) . i < (Y_axis l) . j
then A9: ( [n,i] in Indices (GoB v1,v2) & [n,j] in Indices (GoB v1,v2) ) by A3, A4, A5, A6, ZFMISC_1:106;
reconsider r = v1 . n, s1 = v2 . i, s2 = v2 . j as Real ;
( (GoB v1,v2) * n,i = |[r,s1]| & (GoB v1,v2) * n,j = |[r,s2]| ) by A9, Def1;
then A10: ( ((GoB v1,v2) * n,i) `2 = s1 & ((GoB v1,v2) * n,j) `2 = s2 ) by EUCLID:56;
( l /. i = l . i & l /. j = l . j ) by A7, A8, PARTFUN1:def 8;
then ( l /. i = (GoB v1,v2) * n,i & l /. j = (GoB v1,v2) * n,j ) by A6, A8, MATRIX_1:def 8;
then ( (Y_axis l) . i = s1 & (Y_axis l) . j = s2 & s1 < s2 ) by A1, A2, A6, A8, A10, GOBOARD1:def 4, SEQM_3:def 1;
hence (Y_axis l) . i < (Y_axis l) . j ; :: thesis: verum

end;

hence Y_axis (Line (GoB v1,v2),n) is increasing by SEQM_3:def 1; :: thesis: verum

end;

thus GoB v1,v2 is X_increasing-in-column :: thesis: verum

proof

let n be Element of NAT ; :: according to GOBOARD1:def 9 :: thesis: ( not n in Seg (width (GoB v1,v2)) or X_axis (Col (GoB v1,v2),n) is increasing )
reconsider c = Col (GoB v1,v2),n as FinSequence of (TOP-REAL 2) ;
set x = X_axis c;
assume A11: n in Seg (width (GoB v1,v2)) ; :: thesis: X_axis (Col (GoB v1,v2),n) is increasing
A12: ( len (X_axis c) = len c & len c = len (GoB v1,v2) & dom (X_axis c) = Seg (len (X_axis c)) ) by FINSEQ_1:def 3, GOBOARD1:def 3, MATRIX_1:def 9;
then A13: ( dom (X_axis c) = dom c & dom c = dom (GoB v1,v2) ) by FINSEQ_3:31;

now

let i, j be Element of NAT ; :: thesis: ( i in dom (X_axis c) & j in dom (X_axis c) & i < j implies (X_axis c) . i < (X_axis c) . j )
assume A14: ( i in dom (X_axis c) & j in dom (X_axis c) & i < j ) ; :: thesis: (X_axis c) . i < (X_axis c) . j
then A15: ( [i,n] in Indices (GoB v1,v2) & [j,n] in Indices (GoB v1,v2) ) by A3, A4, A11, A13, ZFMISC_1:106;
reconsider r = v2 . n, s1 = v1 . i, s2 = v1 . j as Real ;
( (GoB v1,v2) * i,n = |[s1,r]| & (GoB v1,v2) * j,n = |[s2,r]| ) by A15, Def1;
then A16: ( ((GoB v1,v2) * i,n) `1 = s1 & ((GoB v1,v2) * j,n) `1 = s2 ) by EUCLID:56;
( c /. i = c . i & c /. j = c . j ) by A13, A14, PARTFUN1:def 8;
then ( c /. i = (GoB v1,v2) * i,n & c /. j = (GoB v1,v2) * j,n ) by A13, A14, MATRIX_1:def 9;
then ( (X_axis c) . i = s1 & (X_axis c) . j = s2 & s1 < s2 ) by A1, A2, A12, A14, A16, GOBOARD1:def 3, SEQM_3:def 1;
hence (X_axis c) . i < (X_axis c) . j ; :: thesis: verum

end;

hence X_axis (Col (GoB v1,v2),n) is increasing by SEQM_3:def 1; :: thesis: verum

end;