let D be non empty set ; :: thesis: for n, i, m, 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 m & j in Seg m & mt . i = mt . j holds
Col (Segm A,nt,mt),i = Col (Segm A,nt,mt),j
let n, i, m, 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 m & j in Seg m & mt . i = mt . j holds
Col (Segm A,nt,mt),i = Col (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 m & j in Seg m & mt . i = mt . j holds
Col (Segm A,nt,mt),i = Col (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 m & j in Seg m & mt . i = mt . j holds
Col (Segm A,nt,mt),i = Col (Segm A,nt,mt),j
let mt be Element of m -tuples_on NAT ; :: thesis: ( i in Seg m & j in Seg m & mt . i = mt . j implies Col (Segm A,nt,mt),i = Col (Segm A,nt,mt),j )
set S = Segm A,nt,mt;
set Ci = Col (Segm A,nt,mt),i;
set Cj = Col (Segm A,nt,mt),j;
assume that
A1: i in Seg m and
A2: j in Seg m and
A3: mt . i = mt . j ; :: thesis: Col (Segm A,nt,mt),i = Col (Segm A,nt,mt),j

A4: now

let k be Nat; :: thesis: ( 1 <= k & k <= len (Segm A,nt,mt) implies (Col (Segm A,nt,mt),i) . k = (Col (Segm A,nt,mt),j) . k )
assume that
A5: 1 <= k and
A6: k <= len (Segm A,nt,mt) ; :: thesis: (Col (Segm A,nt,mt),i) . k = (Col (Segm A,nt,mt),j) . k
k in NAT by ORDINAL1:def 13;
then A7: k in Seg (len (Segm A,nt,mt)) by A5, A6;
then A8: k in Seg n by MATRIX_1:def 3;
then n <> 0 ;
then A9: width (Segm A,nt,mt) = m by Th1;
[k,j] in [:(Seg n),(Seg m):] by A2, A8, ZFMISC_1:106;
then [k,j] in Indices (Segm A,nt,mt) by A9, MATRIX_1:26;
then A10: (Segm A,nt,mt) * k,j = A * (nt . k),(mt . j) by Def1;
[k,i] in [:(Seg n),(Seg m):] by A1, A8, ZFMISC_1:106;
then [k,i] in Indices (Segm A,nt,mt) by A9, MATRIX_1:26;
then A11: (Segm A,nt,mt) * k,i = A * (nt . k),(mt . i) by Def1;
A12: k in dom (Segm A,nt,mt) by A7, FINSEQ_1:def 3;
then (Segm A,nt,mt) * k,i = (Col (Segm A,nt,mt),i) . k by MATRIX_1:def 9;
hence (Col (Segm A,nt,mt),i) . k = (Col (Segm A,nt,mt),j) . k by A3, A12, A11, A10, MATRIX_1:def 9; :: thesis: verum

end;

A13: len (Col (Segm A,nt,mt),j) = len (Segm A,nt,mt) by MATRIX_1:def 9;
len (Col (Segm A,nt,mt),i) = len (Segm A,nt,mt) by MATRIX_1:def 9;
hence Col (Segm A,nt,mt),i = Col (Segm A,nt,mt),j by A13, A4, FINSEQ_1:18; :: thesis: verum