let D be non empty set ; :: thesis: for j being Nat
for A being Matrix of D
for Q being finite without_zero Subset of NAT st j in Seg (card Q) holds
Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j))
let j be Nat; :: thesis: for A being Matrix of D
for Q being finite without_zero Subset of NAT st j in Seg (card Q) holds
Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j))
let A be Matrix of D; :: thesis: for Q being finite without_zero Subset of NAT st j in Seg (card Q) holds
Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j))
let Q be finite without_zero Subset of NAT; :: thesis: ( j in Seg (card Q) implies Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j)) )
assume A1: j in Seg (card Q) ; :: thesis: Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j))
set S = Seg (len A);
set sQ = Sgm Q;
len (Col (A,((Sgm Q) . j))) = len A by MATRIX_0:def 8;
then A2: dom (Col (A,((Sgm Q) . j))) = Seg (len A) by FINSEQ_1:def 3;
Sgm (Seg (len A)) = idseq (len A) by FINSEQ_3:48;
then (Col (A,((Sgm Q) . j))) * (Sgm (Seg (len A))) = Col (A,((Sgm Q) . j)) by A2, RELAT_1:52;
hence Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j)) by A1, Th49; :: thesis: verum