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 & j in Seg n ) and
A2: nt . i = nt . j ; :: thesis: Line (Segm A,nt,mt),i = Line (Segm A,nt,mt),j
A3: ( len (Line (Segm A,nt,mt),i) = width (Segm A,nt,mt) & len (Line (Segm A,nt,mt),j) = width (Segm A,nt,mt) ) by MATRIX_1:def 8;

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 A4: ( 1 <= k & 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 A5: k in Seg (width (Segm A,nt,mt)) by A4;
then ( [i,k] in [:(Seg n),(Seg (width (Segm A,nt,mt))):] & [j,k] in [:(Seg n),(Seg (width (Segm A,nt,mt))):] ) by A1, ZFMISC_1:106;
then ( [i,k] in Indices (Segm A,nt,mt) & [j,k] in Indices (Segm A,nt,mt) ) by MATRIX_1:26;
then ( (Segm A,nt,mt) * i,k = A * (nt . i),(mt . k) & (Segm A,nt,mt) * j,k = A * (nt . j),(mt . k) & (Segm A,nt,mt) * i,k = (Line (Segm A,nt,mt),i) . k & (Segm A,nt,mt) * j,k = (Line (Segm A,nt,mt),j) . k ) by A5, Def1, MATRIX_1:def 8;
hence (Line (Segm A,nt,mt),i) . k = (Line (Segm A,nt,mt),j) . k by A2; :: thesis: verum

end;

hence Line (Segm A,nt,mt),i = Line (Segm A,nt,mt),j by A3, FINSEQ_1:18; :: thesis: verum