let D be non empty set ; for i, j, m, n being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n & j in Seg n & nt . i = nt . j holds
Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)
let i, j, m, n be Nat; for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n & j in Seg n & nt . i = nt . j holds
Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)
let A be Matrix of D; for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n & j in Seg n & nt . i = nt . j holds
Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)
let nt be Element of n -tuples_on NAT; for mt being Element of m -tuples_on NAT st i in Seg n & j in Seg n & nt . i = nt . j holds
Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)
let mt be Element of m -tuples_on NAT; ( i in Seg n & j in Seg n & nt . i = nt . j implies Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j) )
set S = Segm (A,nt,mt);
set Li = Line ((Segm (A,nt,mt)),i);
set Lj = Line ((Segm (A,nt,mt)),j);
assume that
A1:
i in Seg n
and
A2:
j in Seg n
and
A3:
nt . i = nt . j
; Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)
A4:
now for k being Nat st 1 <= k & k <= width (Segm (A,nt,mt)) holds
(Line ((Segm (A,nt,mt)),i)) . k = (Line ((Segm (A,nt,mt)),j)) . klet k be
Nat;
( 1 <= k & k <= width (Segm (A,nt,mt)) implies (Line ((Segm (A,nt,mt)),i)) . k = (Line ((Segm (A,nt,mt)),j)) . k )assume that A5:
1
<= k
and A6:
k <= width (Segm (A,nt,mt))
;
(Line ((Segm (A,nt,mt)),i)) . k = (Line ((Segm (A,nt,mt)),j)) . kA7:
k in Seg (width (Segm (A,nt,mt)))
by A5, A6;
then
[i,k] in [:(Seg n),(Seg (width (Segm (A,nt,mt)))):]
by A1, ZFMISC_1:87;
then
[i,k] in Indices (Segm (A,nt,mt))
by MATRIX_0:25;
then A8:
(Segm (A,nt,mt)) * (
i,
k)
= A * (
(nt . i),
(mt . k))
by Def1;
[j,k] in [:(Seg n),(Seg (width (Segm (A,nt,mt)))):]
by A2, A7, ZFMISC_1:87;
then
[j,k] in Indices (Segm (A,nt,mt))
by MATRIX_0:25;
then A9:
(Segm (A,nt,mt)) * (
j,
k)
= A * (
(nt . j),
(mt . k))
by Def1;
(Segm (A,nt,mt)) * (
i,
k)
= (Line ((Segm (A,nt,mt)),i)) . k
by A7, MATRIX_0:def 7;
hence
(Line ((Segm (A,nt,mt)),i)) . k = (Line ((Segm (A,nt,mt)),j)) . k
by A3, A7, A8, A9, MATRIX_0:def 7;
verum end;
A10:
len (Line ((Segm (A,nt,mt)),j)) = width (Segm (A,nt,mt))
by MATRIX_0:def 7;
len (Line ((Segm (A,nt,mt)),i)) = width (Segm (A,nt,mt))
by MATRIX_0:def 7;
hence
Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)
by A10, A4; verum