let D be non empty set ; :: thesis: for j being Nat
for A being Matrix of D
for Q, P being finite without_zero Subset of NAT st j in Seg (card Q) & P c= Seg (len A) holds
Col (Segm A,P,Q),j = (Col A,((Sgm Q) . j)) * (Sgm P)
let j be Nat; :: thesis: for A being Matrix of D
for Q, P being finite without_zero Subset of NAT st j in Seg (card Q) & P c= Seg (len A) holds
Col (Segm A,P,Q),j = (Col A,((Sgm Q) . j)) * (Sgm P)
let A be Matrix of D; :: thesis: for Q, P being finite without_zero Subset of NAT st j in Seg (card Q) & P c= Seg (len A) holds
Col (Segm A,P,Q),j = (Col A,((Sgm Q) . j)) * (Sgm P)
let Q, P be finite without_zero Subset of NAT ; :: thesis: ( j in Seg (card Q) & P c= Seg (len A) implies Col (Segm A,P,Q),j = (Col A,((Sgm Q) . j)) * (Sgm P) )
assume that
A1: j in Seg (card Q) and
A2: P c= Seg (len A) ; :: thesis: Col (Segm A,P,Q),j = (Col A,((Sgm Q) . j)) * (Sgm P)
rng (Sgm P) = P by A2, FINSEQ_1:def 13;
hence Col (Segm A,P,Q),j = (Col A,((Sgm Q) . j)) * (Sgm P) by A1, A2, Th28; :: thesis: verum