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

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

end;

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