set M = GoB (v1,v2);
A1: width (GoB (v1,v2)) = len v2 by Def1;
A2: len (GoB (v1,v2)) = len v1 by Def1;
then A3: dom (GoB (v1,v2)) = dom v1 by FINSEQ_3:29;
then A4: Indices (GoB (v1,v2)) = [:(dom v1),(Seg (len v2)):] by ;
A5: dom v2 = Seg (len v2) by FINSEQ_1:def 3;
thus GoB (v1,v2) is Y_increasing-in-line :: thesis: GoB (v1,v2) is X_increasing-in-column
proof
let n be Nat; :: according to GOBOARD1:def 6 :: 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 () ;
set y = Y_axis l;
assume A6: n in dom (GoB (v1,v2)) ; :: thesis: Y_axis (Line ((GoB (v1,v2)),n)) is increasing
A7: ( len l = width (GoB (v1,v2)) & dom () = Seg (len ()) ) by ;
A8: len () = len l by GOBOARD1:def 2;
then A9: dom () = dom l by FINSEQ_3:29;
now :: thesis: for i, j being Nat st i in dom () & j in dom () & i < j holds
() . i < () . j
let i, j be Nat; :: thesis: ( i in dom () & j in dom () & i < j implies () . i < () . j )
assume that
A10: i in dom () and
A11: j in dom () and
A12: i < j ; :: thesis: () . i < () . j
reconsider r = v1 . n, s1 = v2 . i, s2 = v2 . j as Real ;
[n,j] in Indices (GoB (v1,v2)) by A1, A3, A4, A6, A8, A7, A11, ZFMISC_1:87;
then (GoB (v1,v2)) * (n,j) = |[r,s2]| by Def1;
then A13: ((GoB (v1,v2)) * (n,j)) `2 = s2 by EUCLID:52;
l /. j = l . j by ;
then l /. j = (GoB (v1,v2)) * (n,j) by ;
then A14: (Y_axis l) . j = s2 by ;
[n,i] in Indices (GoB (v1,v2)) by A1, A3, A4, A6, A8, A7, A10, ZFMISC_1:87;
then (GoB (v1,v2)) * (n,i) = |[r,s1]| by Def1;
then A15: ((GoB (v1,v2)) * (n,i)) `2 = s1 by EUCLID:52;
l /. i = l . i by ;
then l /. i = (GoB (v1,v2)) * (n,i) by ;
then (Y_axis l) . i = s1 by ;
hence (Y_axis l) . i < () . j by A5, A1, A8, A7, A10, A11, A12, A14, SEQM_3:def 1; :: thesis: verum
end;
hence Y_axis (Line ((GoB (v1,v2)),n)) is increasing by SEQM_3:def 1; :: thesis: verum
end;
A16: dom v1 = Seg (len v1) by FINSEQ_1:def 3;
thus GoB (v1,v2) is X_increasing-in-column :: thesis: verum
proof
let n be Nat; :: according to GOBOARD1:def 7 :: 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 () ;
set x = X_axis c;
assume A17: n in Seg (width (GoB (v1,v2))) ; :: thesis: X_axis (Col ((GoB (v1,v2)),n)) is increasing
A18: len () = len c by GOBOARD1:def 1;
then A19: dom () = dom c by FINSEQ_3:29;
A20: len c = len (GoB (v1,v2)) by MATRIX_0:def 8;
then A21: dom c = dom (GoB (v1,v2)) by FINSEQ_3:29;
A22: dom () = Seg (len ()) by FINSEQ_1:def 3;
now :: thesis: for i, j being Nat st i in dom () & j in dom () & i < j holds
() . i < () . j
let i, j be Nat; :: thesis: ( i in dom () & j in dom () & i < j implies () . i < () . j )
assume that
A23: i in dom () and
A24: j in dom () and
A25: i < j ; :: thesis: () . i < () . j
reconsider r = v2 . n, s1 = v1 . i, s2 = v1 . j as Real ;
[j,n] in Indices (GoB (v1,v2)) by ;
then (GoB (v1,v2)) * (j,n) = |[s2,r]| by Def1;
then A26: ((GoB (v1,v2)) * (j,n)) `1 = s2 by EUCLID:52;
c /. j = c . j by ;
then c /. j = (GoB (v1,v2)) * (j,n) by ;
then A27: (X_axis c) . j = s2 by ;
[i,n] in Indices (GoB (v1,v2)) by ;
then (GoB (v1,v2)) * (i,n) = |[s1,r]| by Def1;
then A28: ((GoB (v1,v2)) * (i,n)) `1 = s1 by EUCLID:52;
c /. i = c . i by ;
then c /. i = (GoB (v1,v2)) * (i,n) by ;
then (X_axis c) . i = s1 by ;
hence (X_axis c) . i < () . j by ; :: thesis: verum
end;
hence X_axis (Col ((GoB (v1,v2)),n)) is increasing by SEQM_3:def 1; :: thesis: verum
end;