let D be non empty set ; :: thesis: for j being Nat
for A being Matrix of D
for P, Q 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 P, Q 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 P, Q 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 P, Q 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) )
rng (Sgm P) = P by FINSEQ_1:def 14;
hence ( j in Seg (card Q) & P c= Seg (len A) implies Col ((Segm (A,P,Q)),j) = (Col (A,((Sgm Q) . j))) * (Sgm P) ) by Th28; :: thesis: verum