let D be non empty set ; :: thesis:
let A be Matrix of D; :: thesis:
let P, Q be finite without_zero Subset of NAT; :: thesis:
assume A1: card P = card Q ; :: thesis:

suppose A2: Q = {} ; :: thesis:

then A3: [:Q,P:] = {} by ZFMISC_1:90;
[:P,Q:] = {} by A2, ZFMISC_1:90;
hence ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @) ) by A3; :: thesis:

end;

suppose A4: Q <> {} ; :: thesis:

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

assume A5: [:P,Q:] c= Indices A ; :: thesis:
then A6: P c= Seg (len A) by A1, Th67;
A7: Q c= Seg (width A) by A1, A5, Th67;
then A8: width A <> 0 by A4;
then A9: len (A @) = width A by MATRIX_0:54;
len A = width (A @) by A8, MATRIX_0:54;
hence [:Q,P:] c= Indices (A @) by A1, A7, A9, A6, Th67; :: thesis:

end;

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

assume A10: [:Q,P:] c= Indices (A @) ; :: thesis:
then A11: Q c= Seg (len (A @)) by A1, Th67;
then len (A @) <> 0 by A4;
then width A > 0 by MATRIX_0:def 6;
then A12: len A = width (A @) by MATRIX_0:54;
A13: len (A @) = width A by MATRIX_0:def 6;
P c= Seg (width (A @)) by A1, A10, Th67;
hence [:P,Q:] c= Indices A by A1, A11, A12, A13, Th67; :: thesis:

end;

end;

end;