set p = the Point of (TOP-REAL 2);

take M = <*<* the Point of (TOP-REAL 2)*>*>; :: thesis: ( M is V3() & M is X_equal-in-line & M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )

A1: len M = 1 by MATRIX_0:24;

A2: width M = 1 by MATRIX_0:24;

hence M is V3() by A1, MATRIX_0:def 10; :: thesis: ( M is X_equal-in-line & M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )

thus M is X_equal-in-line :: thesis: ( M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )

assume n in Seg (width M) ; :: thesis: X_axis (Col (M,n)) is increasing

set L = X_axis (Col (M,n));

let k be Nat; :: according to SEQM_3:def 1 :: thesis: for b_{1} being set holds

( not k in dom (X_axis (Col (M,n))) or not b_{1} in dom (X_axis (Col (M,n))) or b_{1} <= k or not (X_axis (Col (M,n))) . b_{1} <= (X_axis (Col (M,n))) . k )

let m be Nat; :: thesis: ( not k in dom (X_axis (Col (M,n))) or not m in dom (X_axis (Col (M,n))) or m <= k or not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k )

assume that

A16: k in dom (X_axis (Col (M,n))) and

A17: m in dom (X_axis (Col (M,n))) and

A18: k < m ; :: thesis: not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k

A19: len (X_axis (Col (M,n))) = len (Col (M,n)) by Def1;

k in Seg (len (X_axis (Col (M,n)))) by A16, FINSEQ_1:def 3;

then k in {1} by A1, A19, FINSEQ_1:2, MATRIX_0:def 8;

then A20: k = 1 by TARSKI:def 1;

m in Seg (len (X_axis (Col (M,n)))) by A17, FINSEQ_1:def 3;

then m in {1} by A1, A19, FINSEQ_1:2, MATRIX_0:def 8;

hence not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k by A18, A20, TARSKI:def 1; :: thesis: verum

take M = <*<* the Point of (TOP-REAL 2)*>*>; :: thesis: ( M is V3() & M is X_equal-in-line & M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )

A1: len M = 1 by MATRIX_0:24;

A2: width M = 1 by MATRIX_0:24;

hence M is V3() by A1, MATRIX_0:def 10; :: thesis: ( M is X_equal-in-line & M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )

thus M is X_equal-in-line :: thesis: ( M is Y_equal-in-column & M is Y_increasing-in-line & M is X_increasing-in-column )

proof

thus
M is Y_equal-in-column
:: thesis: ( M is Y_increasing-in-line & M is X_increasing-in-column )
let n be Nat; :: according to GOBOARD1:def 4 :: thesis: ( n in dom M implies X_axis (Line (M,n)) is constant )

assume n in dom M ; :: thesis: X_axis (Line (M,n)) is constant

set L = X_axis (Line (M,n));

let k be Nat; :: according to SEQM_3:def 10 :: thesis: for b_{1} being set holds

( not k in dom (X_axis (Line (M,n))) or not b_{1} in dom (X_axis (Line (M,n))) or (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . b_{1} )

let m be Nat; :: thesis: ( not k in dom (X_axis (Line (M,n))) or not m in dom (X_axis (Line (M,n))) or (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m )

assume that

A3: k in dom (X_axis (Line (M,n))) and

A4: m in dom (X_axis (Line (M,n))) ; :: thesis: (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m

A5: len (X_axis (Line (M,n))) = len (Line (M,n)) by Def1;

k in Seg (len (X_axis (Line (M,n)))) by A3, FINSEQ_1:def 3;

then k in {1} by A2, A5, FINSEQ_1:2, MATRIX_0:def 7;

then A6: k = 1 by TARSKI:def 1;

m in Seg (len (X_axis (Line (M,n)))) by A4, FINSEQ_1:def 3;

then m in {1} by A2, A5, FINSEQ_1:2, MATRIX_0:def 7;

hence (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m by A6, TARSKI:def 1; :: thesis: verum

end;assume n in dom M ; :: thesis: X_axis (Line (M,n)) is constant

set L = X_axis (Line (M,n));

let k be Nat; :: according to SEQM_3:def 10 :: thesis: for b

( not k in dom (X_axis (Line (M,n))) or not b

let m be Nat; :: thesis: ( not k in dom (X_axis (Line (M,n))) or not m in dom (X_axis (Line (M,n))) or (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m )

assume that

A3: k in dom (X_axis (Line (M,n))) and

A4: m in dom (X_axis (Line (M,n))) ; :: thesis: (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m

A5: len (X_axis (Line (M,n))) = len (Line (M,n)) by Def1;

k in Seg (len (X_axis (Line (M,n)))) by A3, FINSEQ_1:def 3;

then k in {1} by A2, A5, FINSEQ_1:2, MATRIX_0:def 7;

then A6: k = 1 by TARSKI:def 1;

m in Seg (len (X_axis (Line (M,n)))) by A4, FINSEQ_1:def 3;

then m in {1} by A2, A5, FINSEQ_1:2, MATRIX_0:def 7;

hence (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . m by A6, TARSKI:def 1; :: thesis: verum

proof

thus
M is Y_increasing-in-line
:: thesis: M is X_increasing-in-column
let n be Nat; :: according to GOBOARD1:def 5 :: thesis: ( n in Seg (width M) implies Y_axis (Col (M,n)) is constant )

assume n in Seg (width M) ; :: thesis: Y_axis (Col (M,n)) is constant

set L = Y_axis (Col (M,n));

let k be Nat; :: according to SEQM_3:def 10 :: thesis: for b_{1} being set holds

( not k in dom (Y_axis (Col (M,n))) or not b_{1} in dom (Y_axis (Col (M,n))) or (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . b_{1} )

let m be Nat; :: thesis: ( not k in dom (Y_axis (Col (M,n))) or not m in dom (Y_axis (Col (M,n))) or (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m )

assume that

A7: k in dom (Y_axis (Col (M,n))) and

A8: m in dom (Y_axis (Col (M,n))) ; :: thesis: (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m

A9: len (Y_axis (Col (M,n))) = len (Col (M,n)) by Def2;

k in Seg (len (Y_axis (Col (M,n)))) by A7, FINSEQ_1:def 3;

then k in {1} by A1, A9, FINSEQ_1:2, MATRIX_0:def 8;

then A10: k = 1 by TARSKI:def 1;

m in Seg (len (Y_axis (Col (M,n)))) by A8, FINSEQ_1:def 3;

then m in {1} by A1, A9, FINSEQ_1:2, MATRIX_0:def 8;

hence (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m by A10, TARSKI:def 1; :: thesis: verum

end;assume n in Seg (width M) ; :: thesis: Y_axis (Col (M,n)) is constant

set L = Y_axis (Col (M,n));

let k be Nat; :: according to SEQM_3:def 10 :: thesis: for b

( not k in dom (Y_axis (Col (M,n))) or not b

let m be Nat; :: thesis: ( not k in dom (Y_axis (Col (M,n))) or not m in dom (Y_axis (Col (M,n))) or (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m )

assume that

A7: k in dom (Y_axis (Col (M,n))) and

A8: m in dom (Y_axis (Col (M,n))) ; :: thesis: (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m

A9: len (Y_axis (Col (M,n))) = len (Col (M,n)) by Def2;

k in Seg (len (Y_axis (Col (M,n)))) by A7, FINSEQ_1:def 3;

then k in {1} by A1, A9, FINSEQ_1:2, MATRIX_0:def 8;

then A10: k = 1 by TARSKI:def 1;

m in Seg (len (Y_axis (Col (M,n)))) by A8, FINSEQ_1:def 3;

then m in {1} by A1, A9, FINSEQ_1:2, MATRIX_0:def 8;

hence (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . m by A10, TARSKI:def 1; :: thesis: verum

proof

let n be Nat; :: according to GOBOARD1:def 7 :: thesis: ( n in Seg (width M) implies X_axis (Col (M,n)) is increasing )
let n be Nat; :: according to GOBOARD1:def 6 :: thesis: ( n in dom M implies Y_axis (Line (M,n)) is increasing )

assume n in dom M ; :: thesis: Y_axis (Line (M,n)) is increasing

set L = Y_axis (Line (M,n));

let k be Nat; :: according to SEQM_3:def 1 :: thesis: for b_{1} being set holds

( not k in dom (Y_axis (Line (M,n))) or not b_{1} in dom (Y_axis (Line (M,n))) or b_{1} <= k or not (Y_axis (Line (M,n))) . b_{1} <= (Y_axis (Line (M,n))) . k )

let m be Nat; :: thesis: ( not k in dom (Y_axis (Line (M,n))) or not m in dom (Y_axis (Line (M,n))) or m <= k or not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k )

assume that

A11: k in dom (Y_axis (Line (M,n))) and

A12: m in dom (Y_axis (Line (M,n))) and

A13: k < m ; :: thesis: not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k

A14: len (Y_axis (Line (M,n))) = len (Line (M,n)) by Def2;

k in Seg (len (Y_axis (Line (M,n)))) by A11, FINSEQ_1:def 3;

then k in {1} by A2, A14, FINSEQ_1:2, MATRIX_0:def 7;

then A15: k = 1 by TARSKI:def 1;

m in Seg (len (Y_axis (Line (M,n)))) by A12, FINSEQ_1:def 3;

then m in {1} by A2, A14, FINSEQ_1:2, MATRIX_0:def 7;

hence not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k by A13, A15, TARSKI:def 1; :: thesis: verum

end;assume n in dom M ; :: thesis: Y_axis (Line (M,n)) is increasing

set L = Y_axis (Line (M,n));

let k be Nat; :: according to SEQM_3:def 1 :: thesis: for b

( not k in dom (Y_axis (Line (M,n))) or not b

let m be Nat; :: thesis: ( not k in dom (Y_axis (Line (M,n))) or not m in dom (Y_axis (Line (M,n))) or m <= k or not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k )

assume that

A11: k in dom (Y_axis (Line (M,n))) and

A12: m in dom (Y_axis (Line (M,n))) and

A13: k < m ; :: thesis: not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k

A14: len (Y_axis (Line (M,n))) = len (Line (M,n)) by Def2;

k in Seg (len (Y_axis (Line (M,n)))) by A11, FINSEQ_1:def 3;

then k in {1} by A2, A14, FINSEQ_1:2, MATRIX_0:def 7;

then A15: k = 1 by TARSKI:def 1;

m in Seg (len (Y_axis (Line (M,n)))) by A12, FINSEQ_1:def 3;

then m in {1} by A2, A14, FINSEQ_1:2, MATRIX_0:def 7;

hence not (Y_axis (Line (M,n))) . m <= (Y_axis (Line (M,n))) . k by A13, A15, TARSKI:def 1; :: thesis: verum

assume n in Seg (width M) ; :: thesis: X_axis (Col (M,n)) is increasing

set L = X_axis (Col (M,n));

let k be Nat; :: according to SEQM_3:def 1 :: thesis: for b

( not k in dom (X_axis (Col (M,n))) or not b

let m be Nat; :: thesis: ( not k in dom (X_axis (Col (M,n))) or not m in dom (X_axis (Col (M,n))) or m <= k or not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k )

assume that

A16: k in dom (X_axis (Col (M,n))) and

A17: m in dom (X_axis (Col (M,n))) and

A18: k < m ; :: thesis: not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k

A19: len (X_axis (Col (M,n))) = len (Col (M,n)) by Def1;

k in Seg (len (X_axis (Col (M,n)))) by A16, FINSEQ_1:def 3;

then k in {1} by A1, A19, FINSEQ_1:2, MATRIX_0:def 8;

then A20: k = 1 by TARSKI:def 1;

m in Seg (len (X_axis (Col (M,n)))) by A17, FINSEQ_1:def 3;

then m in {1} by A1, A19, FINSEQ_1:2, MATRIX_0:def 8;

hence not (X_axis (Col (M,n))) . m <= (X_axis (Col (M,n))) . k by A18, A20, TARSKI:def 1; :: thesis: verum