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 & len (Segm A,nt,mt) = n ) by MATRIX_1:def 3, MATRIX_1:def 9;
then A3: ( dom (Col A,(mt . j)) = Seg (len A) & len (Col (Segm A,nt,mt),j) = n & dom (Segm A,nt,mt) = Seg n ) by FINSEQ_1:def 3, MATRIX_1:def 9;
then A4: ( dom ((Col A,(mt . j)) * nt) = dom nt & dom nt = Seg n & dom (Col (Segm A,nt,mt),j) = Seg n & dom A = Seg (len A) ) by A2, FINSEQ_1:def 3, FINSEQ_2:144, RELAT_1:46;

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 A5: 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
A6: ( k = x & 1 <= k & k <= n ) by A4, A5;
( nt . k in rng nt & [k,j] in [:(Seg n),(Seg m):] & m = width (Segm A,nt,mt) ) by A1, A4, A5, A6, Th1, FUNCT_1:def 5, ZFMISC_1:106;
then ( ((Col A,(mt . j)) * nt) . k = (Col A,(mt . j)) . (nt . k) & (Col A,(mt . j)) . (nt . k) = A * (nt . k),(mt . j) & [k,j] in Indices (Segm A,nt,mt) & (Col (Segm A,nt,mt),j) . k = (Segm A,nt,mt) * k,j ) by A2, A3, A4, A5, A6, FUNCT_1:22, MATRIX_1:def 9;
hence (Col (Segm A,nt,mt),j) . x = ((Col A,(mt . j)) * nt) . x by A6, Def1; :: thesis: verum

end;

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