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 A2: Q = {} ; :: thesis: ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @ ) )

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

end;

suppose A4: 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 A5: [:P,Q:] c= Indices A ; :: thesis: [:Q,P:] c= Indices (A @ )
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_2:12;
len A = width (A @ ) by A8, MATRIX_2:12;
hence [:Q,P:] c= Indices (A @ ) by A1, A7, A9, A6, Th67; :: thesis: verum

end;

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

proof

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

end;

end;

end;