let D be non empty set ; :: thesis: for n, j, m 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 n, j, m 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_1:def 9;
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:46;
A4: dom nt = Seg n by FINSEQ_2:144;
A5: len (Segm A,nt,mt) = n by MATRIX_1:def 3;
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_1:def 9;
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

let x be set ; :: 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 Element of 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_1:def 9;
nt . k in rng nt by A4, A7, A9, A10, FUNCT_1:def 5;
then A14: (Col A,(mt . j)) . (nt . k) = A * (nt . k),(mt . j) by A2, A8, MATRIX_1:def 9;
[k,j] in [:(Seg n),(Seg m):] by A1, A7, A9, A10, ZFMISC_1:106;
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:22;
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, FUNCT_1:9; :: thesis: verum