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:90;
[:P,Q:] = {} by A2, ZFMISC_1:90;
hence ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @) ) by A3; :: 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_0:54;
len A = width (A @) by A8, MATRIX_0:54;
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_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: verum

end;

end;

end;