let D be non empty set ; 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; 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; 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; 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; ( 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
; Col ((Segm (A,nt,mt)),i) = Col ((Segm (A,nt,mt)),j)
A4:
now 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)) . klet k be
Nat;
( 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))
;
(Col ((Segm (A,nt,mt)),i)) . k = (Col ((Segm (A,nt,mt)),j)) . kA7:
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;
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; verum