let D be non empty set ; :: thesis: for A being Matrix of D
for P, Q, P1, Q1 being finite without_zero Subset of NAT holds
not ( ( P = {} implies Q = {} ) & ( Q = {} implies P = {} ) & [:P,Q:] c= Indices (Segm A,P1,Q1) & ( for P2, Q2 being finite without_zero Subset of NAT holds
( not P2 c= P1 or not Q2 c= Q1 or not P2 = (Sgm P1) .: P or not Q2 = (Sgm Q1) .: Q or not card P2 = card P or not card Q2 = card Q or not Segm (Segm A,P1,Q1),P,Q = Segm A,P2,Q2 ) ) )
let A be Matrix of D; :: thesis: for P, Q, P1, Q1 being finite without_zero Subset of NAT holds
not ( ( P = {} implies Q = {} ) & ( Q = {} implies P = {} ) & [:P,Q:] c= Indices (Segm A,P1,Q1) & ( for P2, Q2 being finite without_zero Subset of NAT holds
( not P2 c= P1 or not Q2 c= Q1 or not P2 = (Sgm P1) .: P or not Q2 = (Sgm Q1) .: Q or not card P2 = card P or not card Q2 = card Q or not Segm (Segm A,P1,Q1),P,Q = Segm A,P2,Q2 ) ) )
let P, Q, P1, Q1 be finite without_zero Subset of NAT ; :: thesis: not ( ( P = {} implies Q = {} ) & ( Q = {} implies P = {} ) & [:P,Q:] c= Indices (Segm A,P1,Q1) & ( for P2, Q2 being finite without_zero Subset of NAT holds
( not P2 c= P1 or not Q2 c= Q1 or not P2 = (Sgm P1) .: P or not Q2 = (Sgm Q1) .: Q or not card P2 = card P or not card Q2 = card Q or not Segm (Segm A,P1,Q1),P,Q = Segm A,P2,Q2 ) ) )
assume that
A1: ( P = {} iff Q = {} ) and
A2: [:P,Q:] c= Indices (Segm A,P1,Q1) ; :: thesis: ex P2, Q2 being finite without_zero Subset of NAT st
( P2 c= P1 & Q2 c= Q1 & P2 = (Sgm P1) .: P & Q2 = (Sgm Q1) .: Q & card P2 = card P & card Q2 = card Q & Segm (Segm A,P1,Q1),P,Q = Segm A,P2,Q2 )
set S = Segm A,P1,Q1;

A3: now

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

suppose P = {} ; :: thesis: ( P c= Seg (card P1) & Q c= Seg (card Q1) )

hence ( P c= Seg (card P1) & Q c= Seg (card Q1) ) by A1, XBOOLE_1:2; :: thesis: verum

end;

suppose A4: P <> {} ; :: thesis: ( P c= Seg (card P1) & Q c= Seg (card Q1) )

then ( [:P,Q:] <> {} & Indices (Segm A,P1,Q1) = [:(Seg (len (Segm A,P1,Q1))),(Seg (width (Segm A,P1,Q1))):] ) by A1, FINSEQ_1:def 3;
then A5: ( P c= Seg (len (Segm A,P1,Q1)) & Q c= Seg (width (Segm A,P1,Q1)) ) by A2, ZFMISC_1:138;
then ( len (Segm A,P1,Q1) <> 0 & len (Segm A,P1,Q1) = card P1 ) by A4, MATRIX_1:def 3;
hence ( P c= Seg (card P1) & Q c= Seg (card Q1) ) by A5, Th1; :: thesis: verum

end;

end;

end;

consider k being Nat such that
A6: P1 c= Seg k by Th43;
consider k being Nat such that
A7: Q1 c= Seg k by Th43;
set SP = Sgm P1;
set SQ = Sgm Q1;
A8: ( dom (Sgm P1) = Seg (card P1) & rng (Sgm P1) = P1 & Sgm P1 is without_repeated_line & dom (Sgm Q1) = Seg (card Q1) & rng (Sgm Q1) = Q1 & Sgm Q1 is without_repeated_line ) by A6, A7, FINSEQ_1:def 13, FINSEQ_3:45, FINSEQ_3:99;
then A9: ( (Sgm P1) .: P c= P1 & not 0 in P1 & (Sgm Q1) .: Q c= Q1 & not 0 in Q1 ) by RELAT_1:144;
then ( (Sgm P1) .: P is finite & (Sgm P1) .: P c= NAT & not 0 in (Sgm P1) .: P & (Sgm Q1) .: Q is finite & (Sgm Q1) .: Q c= NAT & not 0 in (Sgm Q1) .: Q ) by XBOOLE_1:1;
then reconsider P2 = (Sgm P1) .: P, Q2 = (Sgm Q1) .: Q as finite without_zero Subset of NAT by PSCOMP_1:def 1;
( (Sgm P1) " P2 = P & (Sgm Q1) " Q2 = Q & P,P2 are_equipotent & Q,Q2 are_equipotent ) by A3, A8, CARD_1:60, FUNCT_1:164;
then ( Segm (Segm A,P1,Q1),P,Q = Segm A,P2,Q2 & card P = card P2 & card Q = card Q2 ) by A9, Th56, CARD_1:21;
hence ex P2, Q2 being finite without_zero Subset of NAT st
( P2 c= P1 & Q2 c= Q1 & P2 = (Sgm P1) .: P & Q2 = (Sgm Q1) .: Q & card P2 = card P & card Q2 = card Q & Segm (Segm A,P1,Q1),P,Q = Segm A,P2,Q2 ) by A9; :: thesis: verum