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 )
proof
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 b1 being set holds
( not k in dom (X_axis (Line (M,n))) or not b1 in dom (X_axis (Line (M,n))) or (X_axis (Line (M,n))) . k = (X_axis (Line (M,n))) . b1 )
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;
thus M is Y_equal-in-column :: thesis: ( M is Y_increasing-in-line & M is X_increasing-in-column )
proof
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 b1 being set holds
( not k in dom (Y_axis (Col (M,n))) or not b1 in dom (Y_axis (Col (M,n))) or (Y_axis (Col (M,n))) . k = (Y_axis (Col (M,n))) . b1 )
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;
thus M is Y_increasing-in-line :: thesis: M is X_increasing-in-column
proof
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 b1 being set holds
( not k in dom (Y_axis (Line (M,n))) or not b1 in dom (Y_axis (Line (M,n))) or b1 <= k or not (Y_axis (Line (M,n))) . b1 <= (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;
let n be Nat; :: according to GOBOARD1:def 7 :: thesis: ( n in Seg (width M) implies X_axis (Col (M,n)) is increasing )
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 b1 being set holds
( not k in dom (X_axis (Col (M,n))) or not b1 in dom (X_axis (Col (M,n))) or b1 <= k or not (X_axis (Col (M,n))) . b1 <= (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