let D be non empty set ; :: thesis: for 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 j in Seg m & rng nt c= Seg (len A) holds
Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt
let 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 j in Seg m & rng nt c= Seg (len A) holds
Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt
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 j in Seg m & rng nt c= Seg (len A) holds
Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt
let nt be Element of n -tuples_on NAT; :: thesis: for mt being Element of m -tuples_on NAT st j in Seg m & rng nt c= Seg (len A) holds
Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt
let mt be Element of m -tuples_on NAT; :: thesis: ( j in Seg m & rng nt c= Seg (len A) implies Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt )
set S = Segm (A,nt,mt);
set Cj = Col ((Segm (A,nt,mt)),j);
set CA = Col (A,(mt . j));
assume that
A1: j in Seg m and
A2: rng nt c= Seg (len A) ; :: thesis: Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt
len (Col (A,(mt . j))) = len A by MATRIX_0:def 8;
then dom (Col (A,(mt . j))) = Seg (len A) by FINSEQ_1:def 3;
then A3: dom ((Col (A,(mt . j))) * nt) = dom nt by A2, RELAT_1:27;
A4: dom nt = Seg n by FINSEQ_2:124;
A5: len (Segm (A,nt,mt)) = n by MATRIX_0:def 2;
then A6: dom (Segm (A,nt,mt)) = Seg n by FINSEQ_1:def 3;
len (Col ((Segm (A,nt,mt)),j)) = n by A5, MATRIX_0:def 8;
then A7: dom (Col ((Segm (A,nt,mt)),j)) = Seg n by FINSEQ_1:def 3;
A8: dom A = Seg (len A) by FINSEQ_1:def 3;

now :: thesis: for x being object st x in dom (Col ((Segm (A,nt,mt)),j)) holds
(Col ((Segm (A,nt,mt)),j)) . x = ((Col (A,(mt . j))) * nt) . x

let x be object ; :: thesis: ( x in dom (Col ((Segm (A,nt,mt)),j)) implies (Col ((Segm (A,nt,mt)),j)) . x = ((Col (A,(mt . j))) * nt) . x )
assume A9: x in dom (Col ((Segm (A,nt,mt)),j)) ; :: thesis: (Col ((Segm (A,nt,mt)),j)) . x = ((Col (A,(mt . j))) * nt) . x
consider k being Nat such that
A10: k = x and
A11: 1 <= k and
A12: k <= n by A7, A9;
A13: (Col ((Segm (A,nt,mt)),j)) . k = (Segm (A,nt,mt)) * (k,j) by A6, A7, A9, A10, MATRIX_0:def 8;
nt . k in rng nt by A4, A7, A9, A10, FUNCT_1:def 3;
then A14: (Col (A,(mt . j))) . (nt . k) = A * ((nt . k),(mt . j)) by A2, A8, MATRIX_0:def 8;
[k,j] in [:(Seg n),(Seg m):] by A1, A7, A9, A10, ZFMISC_1:87;
then A15: [k,j] in Indices (Segm (A,nt,mt)) by A6, A11, A12, Th1;
((Col (A,(mt . j))) * nt) . k = (Col (A,(mt . j))) . (nt . k) by A3, A4, A7, A9, A10, FUNCT_1:12;
hence (Col ((Segm (A,nt,mt)),j)) . x = ((Col (A,(mt . j))) * nt) . x by A10, A14, A15, A13, Def1; :: thesis: verum

end;

hence Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt by A3, A4, A7; :: thesis: verum