let D be non empty set ; :: thesis: for m, i, n, j 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 m, i, n, j 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

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
k in NAT by ORDINAL1:def 13;
then 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:106;
then [i,k] in Indices (Segm A,nt,mt) by MATRIX_1:26;
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:106;
then [j,k] in Indices (Segm A,nt,mt) by MATRIX_1:26;
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_1:def 8;
hence (Line (Segm A,nt,mt),i) . k = (Line (Segm A,nt,mt),j) . k by A3, A7, A8, A9, MATRIX_1:def 8; :: thesis: verum

end;

A10: len (Line (Segm A,nt,mt),j) = width (Segm A,nt,mt) by MATRIX_1:def 8;
len (Line (Segm A,nt,mt),i) = width (Segm A,nt,mt) by MATRIX_1:def 8;
hence Line (Segm A,nt,mt),i = Line (Segm A,nt,mt),j by A10, A4, FINSEQ_1:18; :: thesis: verum