let M be X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2); for x being set
for n, m being Nat st x in rng (Line (M,n)) & x in rng (Line (M,m)) & n in dom M & m in dom M holds
n = m
assume
ex x being set ex n, m being Nat st
( x in rng (Line (M,n)) & x in rng (Line (M,m)) & n in dom M & m in dom M & not n = m )
; contradiction
then consider x being set , n, m being Nat such that
A1:
x in rng (Line (M,n))
and
A2:
x in rng (Line (M,m))
and
A3:
n in dom M
and
A4:
m in dom M
and
A5:
n <> m
;
A6:
( n < m or m < n )
by A5, XXREAL_0:1;
A7:
X_axis (Line (M,m)) is constant
by A4, Def3;
reconsider Ln = Line (M,n), Lm = Line (M,m) as FinSequence of (TOP-REAL 2) ;
consider i being Nat such that
A8:
i in dom Ln
and
A9:
Ln . i = x
by A1, FINSEQ_2:10;
set C = X_axis (Col (M,i));
A10:
len Ln = width M
by MATRIX_0:def 7;
reconsider Mi = Col (M,i) as FinSequence of (TOP-REAL 2) ;
A11:
(Col (M,i)) . n = M * (n,i)
by A3, MATRIX_0:def 8;
A12:
len (Col (M,i)) = len M
by MATRIX_0:def 8;
then
n in dom (Col (M,i))
by A3, FINSEQ_3:29;
then A13:
M * (n,i) = Mi /. n
by A11, PARTFUN1:def 6;
A14:
(Col (M,i)) . m = M * (m,i)
by A4, MATRIX_0:def 8;
A15:
dom M = Seg (len M)
by FINSEQ_1:def 3;
then
m in dom (Col (M,i))
by A4, A12, FINSEQ_1:def 3;
then A16:
M * (m,i) = Mi /. m
by A14, PARTFUN1:def 6;
consider j being Nat such that
A17:
j in dom Lm
and
A18:
Lm . j = x
by A2, FINSEQ_2:10;
A19:
( len (X_axis (Col (M,i))) = len (Col (M,i)) & dom (X_axis (Col (M,i))) = Seg (len (X_axis (Col (M,i)))) )
by Def1, FINSEQ_1:def 3;
A20:
Seg (len Ln) = dom Ln
by FINSEQ_1:def 3;
then A21:
X_axis (Col (M,i)) is increasing
by A8, A10, Def6;
A22:
len Lm = width M
by MATRIX_0:def 7;
then A23:
i in dom Lm
by A8, A10, FINSEQ_3:29;
Lm . i = M * (m,i)
by A8, A10, A20, MATRIX_0:def 7;
then A24:
Lm /. i = M * (m,i)
by A23, PARTFUN1:def 6;
A25:
dom (X_axis Lm) = Seg (len (X_axis Lm))
by FINSEQ_1:def 3;
Ln . i = M * (n,i)
by A8, A10, A20, MATRIX_0:def 7;
then reconsider p = x as Point of (TOP-REAL 2) by A9;
A26:
Lm /. j = p
by A17, A18, PARTFUN1:def 6;
A27:
len (X_axis Lm) = len Lm
by Def1;
then A28:
j in dom (X_axis Lm)
by A17, FINSEQ_3:29;
Seg (len Lm) = dom Lm
by FINSEQ_1:def 3;
then A29:
j in dom (X_axis Lm)
by A17, A25, Def1;
i in dom (X_axis Lm)
by A8, A10, A22, A27, FINSEQ_3:29;
then
(X_axis Lm) . i = (X_axis Lm) . j
by A7, A28;
then A30: (M * (m,i)) `1 =
(X_axis Lm) . j
by A8, A25, A10, A22, A27, A20, A24, Def1
.=
p `1
by A29, A26, Def1
;
(M * (n,i)) `1 = p `1
by A8, A9, A10, A20, MATRIX_0:def 7;
then (X_axis (Col (M,i))) . n =
p `1
by A3, A15, A12, A19, A13, Def1
.=
(X_axis (Col (M,i))) . m
by A4, A15, A12, A19, A30, A16, Def1
;
hence
contradiction
by A3, A4, A15, A21, A12, A19, A6; verum