consider p being Point of (TOP-REAL 2);
take M = <*<*p*>*>; :: thesis: ( not M is empty-yielding & 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_1:25;
A2:
width M = 1
by MATRIX_1:25;
hence
not M is empty-yielding
by A1, Def5; :: 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
Element of
NAT ;
:: according to GOBOARD1:def 6 :: 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
Element of
NAT ;
:: according to GOBOARD1:def 2 :: thesis: for m being Element of NAT st k in dom (X_axis (Line M,n)) & m in dom (X_axis (Line M,n)) holds
(X_axis (Line M,n)) . k = (X_axis (Line M,n)) . mlet m be
Element of
NAT ;
:: thesis: ( k in dom (X_axis (Line M,n)) & m in dom (X_axis (Line M,n)) implies (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 Def3;
k in Seg (len (X_axis (Line M,n)))
by A3, FINSEQ_1:def 3;
then
k in {1}
by A2, A5, FINSEQ_1:4, MATRIX_1:def 8;
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:4, MATRIX_1:def 8;
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
Element of
NAT ;
:: according to GOBOARD1:def 7 :: 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
Element of
NAT ;
:: according to GOBOARD1:def 2 :: thesis: for m being Element of NAT st k in dom (Y_axis (Col M,n)) & m in dom (Y_axis (Col M,n)) holds
(Y_axis (Col M,n)) . k = (Y_axis (Col M,n)) . mlet m be
Element of
NAT ;
:: thesis: ( k in dom (Y_axis (Col M,n)) & m in dom (Y_axis (Col M,n)) implies (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 Def4;
k in Seg (len (Y_axis (Col M,n)))
by A7, FINSEQ_1:def 3;
then
k in {1}
by A1, A9, FINSEQ_1:4, MATRIX_1:def 9;
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:4, MATRIX_1:def 9;
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
Element of
NAT ;
:: according to GOBOARD1:def 8 :: 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
Element of
NAT ;
:: according to SEQM_3:def 1 :: thesis: for b1 being Element of NAT 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
Element of
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 Def4;
k in Seg (len (Y_axis (Line M,n)))
by A11, FINSEQ_1:def 3;
then
k in {1}
by A2, A14, FINSEQ_1:4, MATRIX_1:def 8;
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:4, MATRIX_1:def 8;
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 Element of NAT ; :: according to GOBOARD1:def 9 :: 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 Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for b1 being Element of NAT 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 Element of 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 Def3;
k in Seg (len (X_axis (Col M,n)))
by A16, FINSEQ_1:def 3;
then
k in {1}
by A1, A19, FINSEQ_1:4, MATRIX_1:def 9;
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:4, MATRIX_1:def 9;
hence
not (X_axis (Col M,n)) . m <= (X_axis (Col M,n)) . k
by A18, A20, TARSKI:def 1; :: thesis: verum