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) @ )
assume that
A1: [:P,Q:] c= Indices A and
A2: ( card Q = 0 implies card P = 0 ) ; :: thesis: Segm A,P,Q = (Segm (A @ ),Q,P) @
ex m being Nat st Q c= Seg m by Th43;
then A3: rng (Sgm Q) = Q by FINSEQ_1:def 13;
ex n being Nat st P c= Seg n by Th43;
then rng (Sgm P) = P by FINSEQ_1:def 13;
hence Segm A,P,Q = (Segm (A @ ),Q,P) @ by A1, A2, A3, Th19; :: thesis: verum