let D be non empty set ; :: thesis: for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A & ( card Q = 0 implies card P = 0 ) holds
Segm (A,P,Q) = (Segm ((A @),Q,P)) @
let A be Matrix of D; :: thesis: for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A & ( card Q = 0 implies card P = 0 ) holds
Segm (A,P,Q) = (Segm ((A @),Q,P)) @
let P, Q be finite without_zero Subset of NAT; :: thesis: ( [:P,Q:] c= Indices A & ( card Q = 0 implies card P = 0 ) implies Segm (A,P,Q) = (Segm ((A @),Q,P)) @ )
( rng (Sgm Q) = Q & rng (Sgm P) = P ) by FINSEQ_1:def 14;
hence ( [:P,Q:] c= Indices A & ( card Q = 0 implies card P = 0 ) implies Segm (A,P,Q) = (Segm ((A @),Q,P)) @ ) by Th19; :: thesis: verum