let D be non empty set ; :: thesis: for A being Matrix of D
for P, P1, Q, 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, P1, Q, 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, P1, Q, 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 :: thesis: ( P c= Seg (card P1) & Q c= Seg (card Q1) )
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; :: thesis: verum
end;
suppose A4: P <> {} ; :: thesis: ( P c= Seg (card P1) & Q c= Seg (card Q1) )
then A5: Q c= Seg (width (Segm (A,P1,Q1))) by A2, ZFMISC_1:114;
A6: len (Segm (A,P1,Q1)) = card P1 by MATRIX_0:def 2;
A7: Indices (Segm (A,P1,Q1)) = [:(Seg (len (Segm (A,P1,Q1)))),(Seg (width (Segm (A,P1,Q1)))):] by FINSEQ_1:def 3;
then len (Segm (A,P1,Q1)) <> 0 by A1, A2, A4;
hence ( P c= Seg (card P1) & Q c= Seg (card Q1) ) by A1, A2, A7, A5, A6, Th1, ZFMISC_1:114; :: thesis: verum
end;
end;
end;
set SQ = Sgm Q1;
set SP = Sgm P1;
A8: ex k being Nat st P1 c= Seg k by Th43;
then A9: Sgm P1 is one-to-one by FINSEQ_3:92;
A10: ex k being Nat st Q1 c= Seg k by Th43;
then A11: Sgm Q1 is one-to-one by FINSEQ_3:92;
A12: rng (Sgm Q1) = Q1 by A10, FINSEQ_1:def 13;
then A13: (Sgm Q1) .: Q c= Q1 by RELAT_1:111;
then A14: not 0 in (Sgm Q1) .: Q ;
rng (Sgm P1) = P1 by A8, FINSEQ_1:def 13;
then A15: (Sgm P1) .: P c= P1 by RELAT_1:111;
then not 0 in (Sgm P1) .: P ;
then reconsider P2 = (Sgm P1) .: P, Q2 = (Sgm Q1) .: Q as finite without_zero Subset of NAT by A15, A13, A14, MEASURE6:def 2, XBOOLE_1:1;
A16: dom (Sgm Q1) = Seg (card Q1) by A10, FINSEQ_3:40;
then A17: (Sgm Q1) " Q2 = Q by A3, A11, FUNCT_1:94;
A18: dom (Sgm P1) = Seg (card P1) by A8, FINSEQ_3:40;
then P,P2 are_equipotent by A3, A9, CARD_1:33;
then A19: card P = card P2 by CARD_1:5;
Q,Q2 are_equipotent by A3, A16, A11, CARD_1:33;
then A20: card Q = card Q2 by CARD_1:5;
(Sgm P1) " P2 = P by A3, A18, A9, FUNCT_1:94;
then Segm ((Segm (A,P1,Q1)),P,Q) = Segm (A,P2,Q2) by A15, A13, A17, Th56;
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 A12, A15, A19, A20, RELAT_1:111; :: thesis: verum