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