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