let D be non empty set ; :: thesis: for A being Matrix of D
for P, Q being finite without_zero Subset of NAT holds
not ( [:P,Q:] c= Indices A & ( card P = 0 implies card Q = 0 ) & ( card Q = 0 implies card P = 0 ) & not (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 holds
not ( [:P,Q:] c= Indices A & ( card P = 0 implies card Q = 0 ) & ( card Q = 0 implies card P = 0 ) & not (Segm A,P,Q) @ = Segm (A @ ),Q,P )
let P, Q be finite without_zero Subset of NAT ; :: thesis: not ( [:P,Q:] c= Indices A & ( card P = 0 implies card Q = 0 ) & ( card Q = 0 implies card P = 0 ) & not (Segm A,P,Q) @ = Segm (A @ ),Q,P )
assume that
A1: [:P,Q:] c= Indices A and
A2: ( card P = 0 iff card Q = 0 ) ; :: thesis: (Segm A,P,Q) @ = Segm (A @ ),Q,P
consider n being Nat such that
A3: P c= Seg n by Th43;
consider m being Nat such that
A4: Q c= Seg m by Th43;
( rng (Sgm P) = P & rng (Sgm Q) = Q ) by A3, A4, FINSEQ_1:def 13;
hence (Segm A,P,Q) @ = Segm (A @ ),Q,P by A1, A2, Th18; :: thesis: verum