let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)

A4: now :: thesis: 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)) . k

let k be Nat; :: thesis: ( 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)) ; :: thesis: (Line ((Segm (A,nt,mt)),i)) . k = (Line ((Segm (A,nt,mt)),j)) . k
A7: 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; :: thesis: 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; :: thesis: verum