let D be non empty set ; :: thesis: for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st card P = card Q holds
( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @ ) )
let A be Matrix of D; :: thesis: for P, Q being finite without_zero Subset of NAT st card P = card Q holds
( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @ ) )
let P, Q be finite without_zero Subset of NAT ; :: thesis: ( card P = card Q implies ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @ ) ) )
assume A1: card P = card Q ; :: thesis: ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @ ) )

per cases ( Q = {} or Q <> {} ) ;

suppose Q = {} ; :: thesis: ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @ ) )

then ( [:P,Q:] = {} & [:Q,P:] = {} ) by ZFMISC_1:113;
hence ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @ ) ) by XBOOLE_1:2; :: thesis: verum

end;

suppose A2: Q <> {} ; :: thesis: ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @ ) )

thus ( [:P,Q:] c= Indices A implies [:Q,P:] c= Indices (A @ ) ) :: thesis: ( [:Q,P:] c= Indices (A @ ) implies [:P,Q:] c= Indices A )

proof

assume A3: [:P,Q:] c= Indices A ; :: thesis: [:Q,P:] c= Indices (A @ )
then A4: Q c= Seg (width A) by A1, Th67;
then width A <> 0 by A2;
then width A > 0 ;
then ( len A = width (A @ ) & len (A @ ) = width A & P c= Seg (len A) ) by A1, A3, Th67, MATRIX_2:12;
hence [:Q,P:] c= Indices (A @ ) by A1, A4, Th67; :: thesis: verum

end;

thus ( [:Q,P:] c= Indices (A @ ) implies [:P,Q:] c= Indices A ) :: thesis: verum

proof

assume A5: [:Q,P:] c= Indices (A @ ) ; :: thesis: [:P,Q:] c= Indices A
then A6: Q c= Seg (len (A @ )) by A1, Th67;
then ( len (A @ ) <> 0 & len (A @ ) = width A ) by A2, MATRIX_1:def 7;
then width A > 0 ;
then ( len A = width (A @ ) & len (A @ ) = width A & P c= Seg (width (A @ )) ) by A1, A5, Th67, MATRIX_2:12;
hence [:P,Q:] c= Indices A by A1, A6, Th67; :: thesis: verum

end;

end;

end;