let D be non empty set ; 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; 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; ( card P = card Q implies ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @) ) )
assume A1:
card P = card Q
; ( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @) )
per cases
( Q = {} or Q <> {} )
;
suppose A4:
Q <> {}
;
( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @) )thus
(
[:P,Q:] c= Indices A implies
[:Q,P:] c= Indices (A @) )
( [:Q,P:] c= Indices (A @) implies [:P,Q:] c= Indices A )proof
assume A5:
[:P,Q:] c= Indices A
;
[: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;
verum
end; thus
(
[:Q,P:] c= Indices (A @) implies
[:P,Q:] c= Indices A )
verumproof
assume A10:
[:Q,P:] c= Indices (A @)
;
[: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;
verum
end; end; end;