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 sQ = Sgm Q;
set S = Seg (len A);
len (Col A,((Sgm Q) . j)) = len A by MATRIX_1:def 9;
then ( dom (Col A,((Sgm Q) . j)) = Seg (len A) & Sgm (Seg (len A)) = idseq (len A) ) by FINSEQ_1:def 3, FINSEQ_3:54;
then (Col A,((Sgm Q) . j)) * (Sgm (Seg (len A))) = Col A,((Sgm Q) . j) by RELAT_1:78;
hence Col (Segm A,(Seg (len A)),Q),j = Col A,((Sgm Q) . j) by A1, Th49; :: thesis: verum