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 m & j in Seg m & mt . i = mt . j holds
Col ((Segm (A,nt,mt)),i) = Col ((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 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 :: thesis: for k being Nat st 1 <= k & k <= len (Segm (A,nt,mt)) holds
(Col ((Segm (A,nt,mt)),i)) . k = (Col ((Segm (A,nt,mt)),j)) . k

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
A7: k in Seg (len (Segm (A,nt,mt))) by A5, A6;
then A8: k in Seg n by MATRIX_0:def 2;
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:87;
then [k,j] in Indices (Segm (A,nt,mt)) by A9, MATRIX_0:25;
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:87;
then [k,i] in Indices (Segm (A,nt,mt)) by A9, MATRIX_0:25;
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_0:def 8;
hence (Col ((Segm (A,nt,mt)),i)) . k = (Col ((Segm (A,nt,mt)),j)) . k by A3, A12, A11, A10, MATRIX_0:def 8; :: thesis: verum

end;

A13: len (Col ((Segm (A,nt,mt)),j)) = len (Segm (A,nt,mt)) by MATRIX_0:def 8;
len (Col ((Segm (A,nt,mt)),i)) = len (Segm (A,nt,mt)) by MATRIX_0:def 8;
hence Col ((Segm (A,nt,mt)),i) = Col ((Segm (A,nt,mt)),j) by A13, A4; :: thesis: verum