:: HALLMAR1 semantic presentation begin theorem Th1: :: HALLMAR1:1 for X, Y being finite set holds (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y) proof let X, Y be finite set ; ::_thesis: (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y) card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y)) by CARD_2:45; hence (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y) ; ::_thesis: verum end; scheme :: HALLMAR1:sch 1 Regr11{ F1() -> Element of NAT , P1[ set ] } : for k being Element of NAT st 1 <= k & k <= F1() holds P1[k] provided A1: ( P1[F1()] & F1() >= 2 ) and A2: for k being Element of NAT st 1 <= k & k < F1() & P1[k + 1] holds P1[k] proof defpred S1[ Nat] means ( 1 <= $1 & $1 <= F1() & P1[$1] ); assume ex k being Element of NAT st S1[k] ; ::_thesis: contradiction then A3: ex k being Nat st S1[k] ; A4: for l being Nat st S1[l] holds l <= F1() ; consider l being Nat such that A5: S1[l] and A6: for n being Nat st S1[n] holds n <= l from NAT_1:sch_6(A4, A3); A7: l + 1 >= 1 by NAT_1:12; A8: l < F1() by A1, A5, XXREAL_0:1; then A9: l + 1 <= F1() by NAT_1:13; A10: now__::_thesis:_P1[l_+_1] assume P1[l + 1] ; ::_thesis: contradiction then l + 1 <= l by A6, A9, A7; hence contradiction by XREAL_1:29; ::_thesis: verum end; l in NAT by ORDINAL1:def_12; hence contradiction by A2, A5, A8, A10; ::_thesis: verum end; scheme :: HALLMAR1:sch 2 Regr2{ P1[ set ] } : P1[1] provided A1: ex n being Element of NAT st ( n > 1 & P1[n] ) and A2: for k being Element of NAT st k >= 1 & P1[k + 1] holds P1[k] proof consider n being Element of NAT such that A3: n > 1 and A4: P1[n] by A1; n >= 1 + 1 by A3, NAT_1:13; then A5: ( P1[n] & n >= 2 ) by A4; A6: for k being Element of NAT st 1 <= k & k < n & P1[k + 1] holds P1[k] by A2; for k being Element of NAT st 1 <= k & k <= n holds P1[k] from HALLMAR1:sch_1(A5, A6); hence P1[1] by A3; ::_thesis: verum end; registration let F be non empty set ; cluster non empty Relation-like non-empty NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like for FinSequence of bool F; existence ex b1 being FinSequence of bool F st ( not b1 is empty & b1 is non-empty ) proof set x = the non empty Subset of F; take v = <* the non empty Subset of F*>; ::_thesis: ( not v is empty & v is non-empty ) thus not v is empty ; ::_thesis: v is non-empty rng v = { the non empty Subset of F} by FINSEQ_1:39; then not {} in rng v by TARSKI:def_1; hence v is non-empty by RELAT_1:def_9; ::_thesis: verum end; end; theorem Th2: :: HALLMAR1:2 for F being non empty set for f being non-empty FinSequence of bool F for i being Element of NAT st i in dom f holds f . i <> {} proof let F be non empty set ; ::_thesis: for f being non-empty FinSequence of bool F for i being Element of NAT st i in dom f holds f . i <> {} let f be non-empty FinSequence of bool F; ::_thesis: for i being Element of NAT st i in dom f holds f . i <> {} let i be Element of NAT ; ::_thesis: ( i in dom f implies f . i <> {} ) assume A1: i in dom f ; ::_thesis: f . i <> {} assume f . i = {} ; ::_thesis: contradiction then {} in rng f by A1, FUNCT_1:3; hence contradiction by RELAT_1:def_9; ::_thesis: verum end; registration let F be finite set ; let A be FinSequence of bool F; let i be Element of NAT ; clusterA . i -> finite ; coherence A . i is finite proof percases ( i in dom A or not i in dom A ) ; suppose i in dom A ; ::_thesis: A . i is finite then A . i in bool F by PARTFUN1:4; hence A . i is finite ; ::_thesis: verum end; suppose not i in dom A ; ::_thesis: A . i is finite hence A . i is finite by FUNCT_1:def_2; ::_thesis: verum end; end; end; end; begin definition let F be set ; let A be FinSequence of bool F; let J be set ; func union (A,J) -> set means :Def1: :: HALLMAR1:def 1 for x being set holds ( x in it iff ex j being set st ( j in J & j in dom A & x in A . j ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex j being set st ( j in J & j in dom A & x in A . j ) ) proof defpred S1[ set ] means ex j being set st ( j in J & j in dom A & $1 in A . j ); consider X being set such that A1: for x being set holds ( x in X iff ( x in F & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff ex j being set st ( j in J & j in dom A & x in A . j ) ) let x be set ; ::_thesis: ( x in X iff ex j being set st ( j in J & j in dom A & x in A . j ) ) thus ( x in X implies ex j being set st ( j in J & j in dom A & x in A . j ) ) by A1; ::_thesis: ( ex j being set st ( j in J & j in dom A & x in A . j ) implies x in X ) given j being set such that A2: j in J and A3: j in dom A and A4: x in A . j ; ::_thesis: x in X ( rng A c= bool F & A . j in rng A ) by A3, FINSEQ_1:def_4, FUNCT_1:3; hence x in X by A1, A2, A3, A4; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex j being set st ( j in J & j in dom A & x in A . j ) ) ) & ( for x being set holds ( x in b2 iff ex j being set st ( j in J & j in dom A & x in A . j ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex j being set st ( j in J & j in dom A & $1 in A . j ); let A1, A2 be set ; ::_thesis: ( ( for x being set holds ( x in A1 iff ex j being set st ( j in J & j in dom A & x in A . j ) ) ) & ( for x being set holds ( x in A2 iff ex j being set st ( j in J & j in dom A & x in A . j ) ) ) implies A1 = A2 ) assume that A5: for x being set holds ( x in A1 iff ex j being set st ( j in J & j in dom A & x in A . j ) ) and A6: for x being set holds ( x in A2 iff ex j being set st ( j in J & j in dom A & x in A . j ) ) ; ::_thesis: A1 = A2 A7: for x being set holds ( x in A2 iff S1[x] ) by A6; A8: for x being set holds ( x in A1 iff S1[x] ) by A5; A1 = A2 from XBOOLE_0:sch_2(A8, A7); hence A1 = A2 ; ::_thesis: verum end; end; :: deftheorem Def1 defines union HALLMAR1:def_1_:_ for F being set for A being FinSequence of bool F for J, b4 being set holds ( b4 = union (A,J) iff for x being set holds ( x in b4 iff ex j being set st ( j in J & j in dom A & x in A . j ) ) ); theorem Th3: :: HALLMAR1:3 for F being set for A being FinSequence of bool F for J being set holds union (A,J) c= F proof let F be set ; ::_thesis: for A being FinSequence of bool F for J being set holds union (A,J) c= F let A be FinSequence of bool F; ::_thesis: for J being set holds union (A,J) c= F let J be set ; ::_thesis: union (A,J) c= F let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,J) or x in F ) assume x in union (A,J) ; ::_thesis: x in F then consider j being set such that j in J and A1: j in dom A and A2: x in A . j by Def1; ( rng A c= bool F & A . j in rng A ) by A1, FINSEQ_1:def_4, FUNCT_1:3; hence x in F by A2; ::_thesis: verum end; theorem :: HALLMAR1:4 for F being finite set for A being FinSequence of bool F for J, K being set st J c= K holds union (A,J) c= union (A,K) proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for J, K being set st J c= K holds union (A,J) c= union (A,K) let A be FinSequence of bool F; ::_thesis: for J, K being set st J c= K holds union (A,J) c= union (A,K) let J, K be set ; ::_thesis: ( J c= K implies union (A,J) c= union (A,K) ) assume A1: J c= K ; ::_thesis: union (A,J) c= union (A,K) thus union (A,J) c= union (A,K) ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union (A,J) or a in union (A,K) ) assume a in union (A,J) ; ::_thesis: a in union (A,K) then ex j being set st ( j in J & j in dom A & a in A . j ) by Def1; hence a in union (A,K) by A1, Def1; ::_thesis: verum end; end; registration let F be finite set ; let A be FinSequence of bool F; let J be set ; cluster union (A,J) -> finite ; coherence union (A,J) is finite by Th3, FINSET_1:1; end; theorem Th5: :: HALLMAR1:5 for F being finite set for A being FinSequence of bool F for i being Element of NAT st i in dom A holds union (A,{i}) = A . i proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT st i in dom A holds union (A,{i}) = A . i let A be FinSequence of bool F; ::_thesis: for i being Element of NAT st i in dom A holds union (A,{i}) = A . i let i be Element of NAT ; ::_thesis: ( i in dom A implies union (A,{i}) = A . i ) assume A1: i in dom A ; ::_thesis: union (A,{i}) = A . i thus union (A,{i}) c= A . i :: according to XBOOLE_0:def_10 ::_thesis: A . i c= union (A,{i}) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,{i}) or x in A . i ) assume x in union (A,{i}) ; ::_thesis: x in A . i then ex j being set st ( j in {i} & j in dom A & x in A . j ) by Def1; hence x in A . i by TARSKI:def_1; ::_thesis: verum end; thus A . i c= union (A,{i}) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . i or x in union (A,{i}) ) A2: i in {i} by TARSKI:def_1; assume x in A . i ; ::_thesis: x in union (A,{i}) hence x in union (A,{i}) by A1, A2, Def1; ::_thesis: verum end; end; theorem Th6: :: HALLMAR1:6 for F being finite set for A being FinSequence of bool F for i, j being Element of NAT st i in dom A & j in dom A holds union (A,{i,j}) = (A . i) \/ (A . j) proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i, j being Element of NAT st i in dom A & j in dom A holds union (A,{i,j}) = (A . i) \/ (A . j) let A be FinSequence of bool F; ::_thesis: for i, j being Element of NAT st i in dom A & j in dom A holds union (A,{i,j}) = (A . i) \/ (A . j) let i, j be Element of NAT ; ::_thesis: ( i in dom A & j in dom A implies union (A,{i,j}) = (A . i) \/ (A . j) ) assume that A1: i in dom A and A2: j in dom A ; ::_thesis: union (A,{i,j}) = (A . i) \/ (A . j) thus union (A,{i,j}) c= (A . i) \/ (A . j) :: according to XBOOLE_0:def_10 ::_thesis: (A . i) \/ (A . j) c= union (A,{i,j}) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,{i,j}) or x in (A . i) \/ (A . j) ) assume x in union (A,{i,j}) ; ::_thesis: x in (A . i) \/ (A . j) then consider k being set such that A3: ( k in {i,j} & k in dom A & x in A . k ) by Def1; percases ( ( k = i & k in dom A & x in A . k ) or ( k = j & k in dom A & x in A . k ) ) by A3, TARSKI:def_2; suppose ( k = i & k in dom A & x in A . k ) ; ::_thesis: x in (A . i) \/ (A . j) hence x in (A . i) \/ (A . j) by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( k = j & k in dom A & x in A . k ) ; ::_thesis: x in (A . i) \/ (A . j) hence x in (A . i) \/ (A . j) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; thus (A . i) \/ (A . j) c= union (A,{i,j}) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A . i) \/ (A . j) or x in union (A,{i,j}) ) assume A4: x in (A . i) \/ (A . j) ; ::_thesis: x in union (A,{i,j}) percases ( x in A . i or x in A . j ) by A4, XBOOLE_0:def_3; supposeA5: x in A . i ; ::_thesis: x in union (A,{i,j}) i in {i,j} by TARSKI:def_2; hence x in union (A,{i,j}) by A1, A5, Def1; ::_thesis: verum end; supposeA6: x in A . j ; ::_thesis: x in union (A,{i,j}) j in {i,j} by TARSKI:def_2; hence x in union (A,{i,j}) by A2, A6, Def1; ::_thesis: verum end; end; end; end; theorem Th7: :: HALLMAR1:7 for J being set for F being finite set for A being FinSequence of bool F for i being Element of NAT st i in J & i in dom A holds A . i c= union (A,J) proof let J be set ; ::_thesis: for F being finite set for A being FinSequence of bool F for i being Element of NAT st i in J & i in dom A holds A . i c= union (A,J) let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT st i in J & i in dom A holds A . i c= union (A,J) let A be FinSequence of bool F; ::_thesis: for i being Element of NAT st i in J & i in dom A holds A . i c= union (A,J) let i be Element of NAT ; ::_thesis: ( i in J & i in dom A implies A . i c= union (A,J) ) assume A1: ( i in J & i in dom A ) ; ::_thesis: A . i c= union (A,J) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . i or x in union (A,J) ) assume x in A . i ; ::_thesis: x in union (A,J) hence x in union (A,J) by A1, Def1; ::_thesis: verum end; theorem Th8: :: HALLMAR1:8 for J being set for F being finite set for i being Element of NAT for A being FinSequence of bool F st i in J & i in dom A holds union (A,J) = (union (A,(J \ {i}))) \/ (A . i) proof let J be set ; ::_thesis: for F being finite set for i being Element of NAT for A being FinSequence of bool F st i in J & i in dom A holds union (A,J) = (union (A,(J \ {i}))) \/ (A . i) let F be finite set ; ::_thesis: for i being Element of NAT for A being FinSequence of bool F st i in J & i in dom A holds union (A,J) = (union (A,(J \ {i}))) \/ (A . i) let i be Element of NAT ; ::_thesis: for A being FinSequence of bool F st i in J & i in dom A holds union (A,J) = (union (A,(J \ {i}))) \/ (A . i) let A be FinSequence of bool F; ::_thesis: ( i in J & i in dom A implies union (A,J) = (union (A,(J \ {i}))) \/ (A . i) ) assume ( i in J & i in dom A ) ; ::_thesis: union (A,J) = (union (A,(J \ {i}))) \/ (A . i) then A1: A . i c= union (A,J) by Th7; thus union (A,J) c= (union (A,(J \ {i}))) \/ (A . i) :: according to XBOOLE_0:def_10 ::_thesis: (union (A,(J \ {i}))) \/ (A . i) c= union (A,J) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,J) or x in (union (A,(J \ {i}))) \/ (A . i) ) assume x in union (A,J) ; ::_thesis: x in (union (A,(J \ {i}))) \/ (A . i) then consider j being set such that A2: j in J and A3: j in dom A and A4: x in A . j by Def1; percases ( i = j or i <> j ) ; suppose i = j ; ::_thesis: x in (union (A,(J \ {i}))) \/ (A . i) hence x in (union (A,(J \ {i}))) \/ (A . i) by A4, XBOOLE_0:def_3; ::_thesis: verum end; suppose i <> j ; ::_thesis: x in (union (A,(J \ {i}))) \/ (A . i) then not j in {i} by TARSKI:def_1; then j in J \ {i} by A2, XBOOLE_0:def_5; then x in union (A,(J \ {i})) by A3, A4, Def1; hence x in (union (A,(J \ {i}))) \/ (A . i) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; thus (union (A,(J \ {i}))) \/ (A . i) c= union (A,J) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union (A,(J \ {i}))) \/ (A . i) or x in union (A,J) ) assume x in (union (A,(J \ {i}))) \/ (A . i) ; ::_thesis: x in union (A,J) then A5: ( x in union (A,(J \ {i})) or x in A . i ) by XBOOLE_0:def_3; percases ( x in union (A,(J \ {i})) or x in union (A,J) ) by A1, A5; suppose x in union (A,(J \ {i})) ; ::_thesis: x in union (A,J) then ex j being set st ( j in J \ {i} & j in dom A & x in A . j ) by Def1; hence x in union (A,J) by Def1; ::_thesis: verum end; suppose x in union (A,J) ; ::_thesis: x in union (A,J) hence x in union (A,J) ; ::_thesis: verum end; end; end; end; theorem Th9: :: HALLMAR1:9 for J1, J2 being set for F being finite set for i being Element of NAT for A being FinSequence of bool F st i in dom A holds union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2))) proof let J1, J2 be set ; ::_thesis: for F being finite set for i being Element of NAT for A being FinSequence of bool F st i in dom A holds union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2))) let F be finite set ; ::_thesis: for i being Element of NAT for A being FinSequence of bool F st i in dom A holds union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2))) let i be Element of NAT ; ::_thesis: for A being FinSequence of bool F st i in dom A holds union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2))) let A be FinSequence of bool F; ::_thesis: ( i in dom A implies union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2))) ) assume i in dom A ; ::_thesis: union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2))) then A1: union (A,{i}) = A . i by Th5; thus union (A,(({i} \/ J1) \/ J2)) c= (A . i) \/ (union (A,(J1 \/ J2))) :: according to XBOOLE_0:def_10 ::_thesis: (A . i) \/ (union (A,(J1 \/ J2))) c= union (A,(({i} \/ J1) \/ J2)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,(({i} \/ J1) \/ J2)) or x in (A . i) \/ (union (A,(J1 \/ J2))) ) assume x in union (A,(({i} \/ J1) \/ J2)) ; ::_thesis: x in (A . i) \/ (union (A,(J1 \/ J2))) then consider j being set such that A2: j in ({i} \/ J1) \/ J2 and A3: j in dom A and A4: x in A . j by Def1; percases ( i = j or i <> j ) ; suppose i = j ; ::_thesis: x in (A . i) \/ (union (A,(J1 \/ J2))) hence x in (A . i) \/ (union (A,(J1 \/ J2))) by A4, XBOOLE_0:def_3; ::_thesis: verum end; supposeA5: i <> j ; ::_thesis: x in (A . i) \/ (union (A,(J1 \/ J2))) j in {i} \/ (J1 \/ J2) by A2, XBOOLE_1:4; then ( j in {i} or j in J1 \/ J2 ) by XBOOLE_0:def_3; then x in union (A,(J1 \/ J2)) by A3, A4, A5, Def1, TARSKI:def_1; hence x in (A . i) \/ (union (A,(J1 \/ J2))) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; thus (A . i) \/ (union (A,(J1 \/ J2))) c= union (A,(({i} \/ J1) \/ J2)) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A . i) \/ (union (A,(J1 \/ J2))) or x in union (A,(({i} \/ J1) \/ J2)) ) assume A6: x in (A . i) \/ (union (A,(J1 \/ J2))) ; ::_thesis: x in union (A,(({i} \/ J1) \/ J2)) percases ( x in union (A,{i}) or x in union (A,(J1 \/ J2)) ) by A1, A6, XBOOLE_0:def_3; suppose x in union (A,{i}) ; ::_thesis: x in union (A,(({i} \/ J1) \/ J2)) then consider j being set such that A7: j in {i} and A8: ( j in dom A & x in A . j ) by Def1; j in {i} \/ (J1 \/ J2) by A7, XBOOLE_0:def_3; then j in ({i} \/ J1) \/ J2 by XBOOLE_1:4; hence x in union (A,(({i} \/ J1) \/ J2)) by A8, Def1; ::_thesis: verum end; suppose x in union (A,(J1 \/ J2)) ; ::_thesis: x in union (A,(({i} \/ J1) \/ J2)) then consider j being set such that A9: j in J1 \/ J2 and A10: ( j in dom A & x in A . j ) by Def1; j in {i} \/ (J1 \/ J2) by A9, XBOOLE_0:def_3; then j in ({i} \/ J1) \/ J2 by XBOOLE_1:4; hence x in union (A,(({i} \/ J1) \/ J2)) by A10, Def1; ::_thesis: verum end; end; end; end; theorem Th10: :: HALLMAR1:10 for F being finite set for A being FinSequence of bool F for i being Element of NAT for x, y being set st x <> y & x in A . i & y in A . i holds ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT for x, y being set st x <> y & x in A . i & y in A . i holds ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i let A be FinSequence of bool F; ::_thesis: for i being Element of NAT for x, y being set st x <> y & x in A . i & y in A . i holds ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i let i be Element of NAT ; ::_thesis: for x, y being set st x <> y & x in A . i & y in A . i holds ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i let x, y be set ; ::_thesis: ( x <> y & x in A . i & y in A . i implies ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i ) assume that A1: x <> y and A2: x in A . i and A3: y in A . i ; ::_thesis: ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i A . i c= ((A . i) \ {x}) \/ ((A . i) \ {y}) proof {} = {y} \ ({y} \/ {}) by XBOOLE_1:46; then A . i = (A . i) \ ({y} \ {y}) ; then A . i = ((A . i) \ {y}) \/ ((A . i) /\ {y}) by XBOOLE_1:52; then A4: A . i = ((A . i) \ {y}) \/ {y} by A3, ZFMISC_1:46; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A . i or z in ((A . i) \ {x}) \/ ((A . i) \ {y}) ) not x in {y} by A1, TARSKI:def_1; then A5: x in (A . i) \ {y} by A2, XBOOLE_0:def_5; assume z in A . i ; ::_thesis: z in ((A . i) \ {x}) \/ ((A . i) \ {y}) then z in (((A . i) \ {x}) \/ {x}) \/ (((A . i) \ {y}) \/ {y}) by A4, XBOOLE_0:def_3; then z in ((A . i) \ {x}) \/ ({x} \/ ({y} \/ ((A . i) \ {y}))) by XBOOLE_1:4; then z in ((A . i) \ {x}) \/ (({x} \/ {y}) \/ ((A . i) \ {y})) by XBOOLE_1:4; then z in (((A . i) \ {x}) \/ ({y} \/ {x})) \/ ((A . i) \ {y}) by XBOOLE_1:4; then z in ((((A . i) \ {x}) \/ {y}) \/ {x}) \/ ((A . i) \ {y}) by XBOOLE_1:4; then A6: z in (((A . i) \ {x}) \/ {y}) \/ ({x} \/ ((A . i) \ {y})) by XBOOLE_1:4; not y in {x} by A1, TARSKI:def_1; then y in (A . i) \ {x} by A3, XBOOLE_0:def_5; then z in ((A . i) \ {x}) \/ ({x} \/ ((A . i) \ {y})) by A6, ZFMISC_1:40; hence z in ((A . i) \ {x}) \/ ((A . i) \ {y}) by A5, ZFMISC_1:40; ::_thesis: verum end; hence ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i by XBOOLE_0:def_10; ::_thesis: verum end; begin definition let F be finite set ; let A be FinSequence of bool F; let i be Element of NAT ; let x be set ; func Cut (A,i,x) -> FinSequence of bool F means :Def2: :: HALLMAR1:def 2 ( dom it = dom A & ( for k being Element of NAT st k in dom it holds ( ( i = k implies it . k = (A . k) \ {x} ) & ( i <> k implies it . k = A . k ) ) ) ); existence ex b1 being FinSequence of bool F st ( dom b1 = dom A & ( for k being Element of NAT st k in dom b1 holds ( ( i = k implies b1 . k = (A . k) \ {x} ) & ( i <> k implies b1 . k = A . k ) ) ) ) proof A . i c= F proof percases ( i in dom A or not i in dom A ) ; suppose i in dom A ; ::_thesis: A . i c= F then A . i in bool F by FINSEQ_2:11; hence A . i c= F ; ::_thesis: verum end; suppose not i in dom A ; ::_thesis: A . i c= F then A . i = {} by FUNCT_1:def_2; hence A . i c= F by XBOOLE_1:2; ::_thesis: verum end; end; end; then reconsider EX = (A . i) \ {x} as Subset of F by XBOOLE_1:1; set XX = A +* (i,EX); reconsider XX = A +* (i,EX) as FinSequence of bool F ; take XX ; ::_thesis: ( dom XX = dom A & ( for k being Element of NAT st k in dom XX holds ( ( i = k implies XX . k = (A . k) \ {x} ) & ( i <> k implies XX . k = A . k ) ) ) ) dom XX = dom A by FUNCT_7:30; hence ( dom XX = dom A & ( for k being Element of NAT st k in dom XX holds ( ( i = k implies XX . k = (A . k) \ {x} ) & ( i <> k implies XX . k = A . k ) ) ) ) by FUNCT_7:31, FUNCT_7:32; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of bool F st dom b1 = dom A & ( for k being Element of NAT st k in dom b1 holds ( ( i = k implies b1 . k = (A . k) \ {x} ) & ( i <> k implies b1 . k = A . k ) ) ) & dom b2 = dom A & ( for k being Element of NAT st k in dom b2 holds ( ( i = k implies b2 . k = (A . k) \ {x} ) & ( i <> k implies b2 . k = A . k ) ) ) holds b1 = b2 proof let f1, f2 be FinSequence of bool F; ::_thesis: ( dom f1 = dom A & ( for k being Element of NAT st k in dom f1 holds ( ( i = k implies f1 . k = (A . k) \ {x} ) & ( i <> k implies f1 . k = A . k ) ) ) & dom f2 = dom A & ( for k being Element of NAT st k in dom f2 holds ( ( i = k implies f2 . k = (A . k) \ {x} ) & ( i <> k implies f2 . k = A . k ) ) ) implies f1 = f2 ) assume that A1: dom f1 = dom A and A2: for k being Element of NAT st k in dom f1 holds ( ( i = k implies f1 . k = (A . k) \ {x} ) & ( i <> k implies f1 . k = A . k ) ) and A3: dom f2 = dom A and A4: for k being Element of NAT st k in dom f2 holds ( ( i = k implies f2 . k = (A . k) \ {x} ) & ( i <> k implies f2 . k = A . k ) ) ; ::_thesis: f1 = f2 for z being Nat st z in dom f1 holds f1 . z = f2 . z proof let z be Nat; ::_thesis: ( z in dom f1 implies f1 . z = f2 . z ) assume A5: z in dom f1 ; ::_thesis: f1 . z = f2 . z percases ( z = i or z <> i ) ; supposeA6: z = i ; ::_thesis: f1 . z = f2 . z then f1 . z = (A . i) \ {x} by A2, A5 .= f2 . z by A1, A3, A4, A5, A6 ; hence f1 . z = f2 . z ; ::_thesis: verum end; supposeA7: z <> i ; ::_thesis: f1 . z = f2 . z then f1 . z = A . z by A2, A5 .= f2 . z by A1, A3, A4, A5, A7 ; hence f1 . z = f2 . z ; ::_thesis: verum end; end; end; hence f1 = f2 by A1, A3, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def2 defines Cut HALLMAR1:def_2_:_ for F being finite set for A being FinSequence of bool F for i being Element of NAT for x being set for b5 being FinSequence of bool F holds ( b5 = Cut (A,i,x) iff ( dom b5 = dom A & ( for k being Element of NAT st k in dom b5 holds ( ( i = k implies b5 . k = (A . k) \ {x} ) & ( i <> k implies b5 . k = A . k ) ) ) ) ); theorem Th11: :: HALLMAR1:11 for F being finite set for A being FinSequence of bool F for i being Element of NAT for x being set st i in dom A & x in A . i holds card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT for x being set st i in dom A & x in A . i holds card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 let A be FinSequence of bool F; ::_thesis: for i being Element of NAT for x being set st i in dom A & x in A . i holds card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 let i be Element of NAT ; ::_thesis: for x being set st i in dom A & x in A . i holds card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 let x be set ; ::_thesis: ( i in dom A & x in A . i implies card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 ) set f = Cut (A,i,x); assume that A1: i in dom A and A2: x in A . i ; ::_thesis: card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 i in dom (Cut (A,i,x)) by A1, Def2; then A3: (Cut (A,i,x)) . i = (A . i) \ {x} by Def2; {x} c= A . i by A2, ZFMISC_1:31; then card ((Cut (A,i,x)) . i) = (card (A . i)) - (card {x}) by A3, CARD_2:44 .= (card (A . i)) - 1 by CARD_2:42 ; hence card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 ; ::_thesis: verum end; theorem Th12: :: HALLMAR1:12 for F being finite set for A being FinSequence of bool F for i being Element of NAT for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i})) proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i})) let A be FinSequence of bool F; ::_thesis: for i being Element of NAT for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i})) let i be Element of NAT ; ::_thesis: for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i})) let x, J be set ; ::_thesis: union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i})) thus union ((Cut (A,i,x)),(J \ {i})) c= union (A,(J \ {i})) :: according to XBOOLE_0:def_10 ::_thesis: union (A,(J \ {i})) c= union ((Cut (A,i,x)),(J \ {i})) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union ((Cut (A,i,x)),(J \ {i})) or z in union (A,(J \ {i})) ) assume z in union ((Cut (A,i,x)),(J \ {i})) ; ::_thesis: z in union (A,(J \ {i})) then consider j being set such that A1: j in J \ {i} and A2: j in dom (Cut (A,i,x)) and A3: z in (Cut (A,i,x)) . j by Def1; not j in {i} by A1, XBOOLE_0:def_5; then i <> j by TARSKI:def_1; then A4: z in A . j by A2, A3, Def2; j in dom A by A2, Def2; hence z in union (A,(J \ {i})) by A1, A4, Def1; ::_thesis: verum end; A5: dom (Cut (A,i,x)) = dom A by Def2; thus union (A,(J \ {i})) c= union ((Cut (A,i,x)),(J \ {i})) ::_thesis: verum proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (A,(J \ {i})) or z in union ((Cut (A,i,x)),(J \ {i})) ) assume z in union (A,(J \ {i})) ; ::_thesis: z in union ((Cut (A,i,x)),(J \ {i})) then consider j being set such that A6: j in J \ {i} and A7: j in dom A and A8: z in A . j by Def1; not j in {i} by A6, XBOOLE_0:def_5; then i <> j by TARSKI:def_1; then (Cut (A,i,x)) . j = A . j by A5, A7, Def2; hence z in union ((Cut (A,i,x)),(J \ {i})) by A5, A6, A7, A8, Def1; ::_thesis: verum end; end; theorem Th13: :: HALLMAR1:13 for F being finite set for A being FinSequence of bool F for i being Element of NAT for x, J being set st not i in J holds union (A,J) = union ((Cut (A,i,x)),J) proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT for x, J being set st not i in J holds union (A,J) = union ((Cut (A,i,x)),J) let A be FinSequence of bool F; ::_thesis: for i being Element of NAT for x, J being set st not i in J holds union (A,J) = union ((Cut (A,i,x)),J) let i be Element of NAT ; ::_thesis: for x, J being set st not i in J holds union (A,J) = union ((Cut (A,i,x)),J) let x, J be set ; ::_thesis: ( not i in J implies union (A,J) = union ((Cut (A,i,x)),J) ) assume A1: not i in J ; ::_thesis: union (A,J) = union ((Cut (A,i,x)),J) thus union (A,J) c= union ((Cut (A,i,x)),J) :: according to XBOOLE_0:def_10 ::_thesis: union ((Cut (A,i,x)),J) c= union (A,J) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (A,J) or z in union ((Cut (A,i,x)),J) ) assume z in union (A,J) ; ::_thesis: z in union ((Cut (A,i,x)),J) then consider j being set such that A2: j in J and A3: j in dom A and A4: z in A . j by Def1; A5: j in dom (Cut (A,i,x)) by A3, Def2; percases ( i = j or i <> j ) ; suppose i = j ; ::_thesis: z in union ((Cut (A,i,x)),J) hence z in union ((Cut (A,i,x)),J) by A1, A2; ::_thesis: verum end; suppose i <> j ; ::_thesis: z in union ((Cut (A,i,x)),J) then (Cut (A,i,x)) . j = A . j by A5, Def2; hence z in union ((Cut (A,i,x)),J) by A2, A4, A5, Def1; ::_thesis: verum end; end; end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union ((Cut (A,i,x)),J) or z in union (A,J) ) assume z in union ((Cut (A,i,x)),J) ; ::_thesis: z in union (A,J) then consider j being set such that A6: j in J and A7: j in dom (Cut (A,i,x)) and A8: z in (Cut (A,i,x)) . j by Def1; A9: j in dom A by A7, Def2; percases ( i = j or i <> j ) ; suppose i = j ; ::_thesis: z in union (A,J) hence z in union (A,J) by A1, A6; ::_thesis: verum end; suppose i <> j ; ::_thesis: z in union (A,J) then (Cut (A,i,x)) . j = A . j by A7, Def2; hence z in union (A,J) by A6, A8, A9, Def1; ::_thesis: verum end; end; end; theorem Th14: :: HALLMAR1:14 for F being finite set for A being FinSequence of bool F for i being Element of NAT for x, J being set st i in dom (Cut (A,i,x)) & i in J holds union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x}) proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT for x, J being set st i in dom (Cut (A,i,x)) & i in J holds union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x}) let A be FinSequence of bool F; ::_thesis: for i being Element of NAT for x, J being set st i in dom (Cut (A,i,x)) & i in J holds union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x}) let i be Element of NAT ; ::_thesis: for x, J being set st i in dom (Cut (A,i,x)) & i in J holds union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x}) let x, J be set ; ::_thesis: ( i in dom (Cut (A,i,x)) & i in J implies union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x}) ) assume that A1: i in dom (Cut (A,i,x)) and A2: i in J ; ::_thesis: union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x}) union ((Cut (A,i,x)),J) = (union ((Cut (A,i,x)),(J \ {i}))) \/ ((Cut (A,i,x)) . i) by A1, A2, Th8 .= (union (A,(J \ {i}))) \/ ((Cut (A,i,x)) . i) by Th12 .= (union (A,(J \ {i}))) \/ ((A . i) \ {x}) by A1, Def2 ; hence union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x}) ; ::_thesis: verum end; begin definition let F be finite set ; let X be FinSequence of bool F; let A be set ; predA is_a_system_of_different_representatives_of X means :Def3: :: HALLMAR1:def 3 ex f being FinSequence of F st ( f = A & dom X = dom f & ( for i being Element of NAT st i in dom f holds f . i in X . i ) & f is one-to-one ); end; :: deftheorem Def3 defines is_a_system_of_different_representatives_of HALLMAR1:def_3_:_ for F being finite set for X being FinSequence of bool F for A being set holds ( A is_a_system_of_different_representatives_of X iff ex f being FinSequence of F st ( f = A & dom X = dom f & ( for i being Element of NAT st i in dom f holds f . i in X . i ) & f is one-to-one ) ); definition let F be finite set ; let A be FinSequence of bool F; attrA is Hall means :Def4: :: HALLMAR1:def 4 for J being finite set st J c= dom A holds card J <= card (union (A,J)); end; :: deftheorem Def4 defines Hall HALLMAR1:def_4_:_ for F being finite set for A being FinSequence of bool F holds ( A is Hall iff for J being finite set st J c= dom A holds card J <= card (union (A,J)) ); registration let F be non empty finite set ; cluster non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like Hall for FinSequence of bool F; existence ex b1 being FinSequence of bool F st ( b1 is Hall & not b1 is empty ) proof set c = the Element of F; reconsider b = { the Element of F} as Element of bool F by ZFMISC_1:31; reconsider f = <*b*> as FinSequence of bool F ; for J being finite set st J c= dom f holds card J <= card (union (f,J)) proof let J be finite set ; ::_thesis: ( J c= dom f implies card J <= card (union (f,J)) ) assume A1: J c= dom f ; ::_thesis: card J <= card (union (f,J)) A2: dom f = {1} by FINSEQ_1:2, FINSEQ_1:38; then A3: ( J = {} or J = {1} ) by A1, ZFMISC_1:33; percases ( J = {} or J = {1} ) by A3; suppose J = {} ; ::_thesis: card J <= card (union (f,J)) then card J = 0 ; hence card J <= card (union (f,J)) by NAT_1:2; ::_thesis: verum end; supposeA4: J = {1} ; ::_thesis: card J <= card (union (f,J)) ( 1 in dom f & 1 in NAT ) by A2, TARSKI:def_1; then union (f,{1}) = f . 1 by Th5 .= b by FINSEQ_1:40 ; then card (union (f,J)) = 1 by A4, CARD_1:30; hence card J <= card (union (f,J)) by A4, CARD_1:30; ::_thesis: verum end; end; end; then f is Hall by Def4; hence ex b1 being FinSequence of bool F st ( b1 is Hall & not b1 is empty ) ; ::_thesis: verum end; end; registration let F be finite set ; cluster Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like Hall for FinSequence of bool F; existence ex b1 being FinSequence of bool F st b1 is Hall proof reconsider f = <*> (bool F) as FinSequence of bool F ; for J being finite set st J c= dom f holds card J <= card (union (f,J)) proof let J be finite set ; ::_thesis: ( J c= dom f implies card J <= card (union (f,J)) ) assume J c= dom f ; ::_thesis: card J <= card (union (f,J)) then card J = 0 ; hence card J <= card (union (f,J)) by NAT_1:2; ::_thesis: verum end; then A1: f is Hall by Def4; take f ; ::_thesis: f is Hall thus f is Hall by A1; ::_thesis: verum end; end; theorem Th15: :: HALLMAR1:15 for F being finite set for A being non empty FinSequence of bool F st A is Hall holds A is non-empty proof let F be finite set ; ::_thesis: for A being non empty FinSequence of bool F st A is Hall holds A is non-empty let A be non empty FinSequence of bool F; ::_thesis: ( A is Hall implies A is non-empty ) assume A1: A is Hall ; ::_thesis: A is non-empty assume not A is non-empty ; ::_thesis: contradiction then {} in rng A by RELAT_1:def_9; then consider i being set such that A2: ( i in dom A & A . i = {} ) by FUNCT_1:def_3; set J = {i}; A3: card {i} = 1 by CARD_2:42; ( {i} c= dom A & card (union (A,{i})) = 0 ) by A2, Th5, CARD_1:27, ZFMISC_1:31; hence contradiction by A1, A3, Def4; ::_thesis: verum end; registration let F be finite set ; cluster non empty Hall -> non empty non-empty for FinSequence of bool F; coherence for b1 being non empty FinSequence of bool F st b1 is Hall holds b1 is non-empty by Th15; end; theorem Th16: :: HALLMAR1:16 for F being finite set for A being FinSequence of bool F for i being Element of NAT st i in dom A & A is Hall holds card (A . i) >= 1 proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT st i in dom A & A is Hall holds card (A . i) >= 1 let A be FinSequence of bool F; ::_thesis: for i being Element of NAT st i in dom A & A is Hall holds card (A . i) >= 1 let i be Element of NAT ; ::_thesis: ( i in dom A & A is Hall implies card (A . i) >= 1 ) assume that A1: i in dom A and A2: A is Hall ; ::_thesis: card (A . i) >= 1 set J = {i}; {i} c= dom A by A1, ZFMISC_1:31; then A3: card {i} <= card (union (A,{i})) by A2, Def4; assume A4: card (A . i) < 1 ; ::_thesis: contradiction union (A,{i}) = A . i by A1, Th5; hence contradiction by A4, A3, CARD_2:42; ::_thesis: verum end; theorem Th17: :: HALLMAR1:17 for F being non empty finite set for A being non empty FinSequence of bool F st ( for i being Element of NAT st i in dom A holds card (A . i) = 1 ) & A is Hall holds ex X being set st X is_a_system_of_different_representatives_of A proof let F be non empty finite set ; ::_thesis: for A being non empty FinSequence of bool F st ( for i being Element of NAT st i in dom A holds card (A . i) = 1 ) & A is Hall holds ex X being set st X is_a_system_of_different_representatives_of A let A be non empty FinSequence of bool F; ::_thesis: ( ( for i being Element of NAT st i in dom A holds card (A . i) = 1 ) & A is Hall implies ex X being set st X is_a_system_of_different_representatives_of A ) assume A1: for i being Element of NAT st i in dom A holds card (A . i) = 1 ; ::_thesis: ( not A is Hall or ex X being set st X is_a_system_of_different_representatives_of A ) reconsider dA = dom A as non empty set ; deffunc H1( Element of dA) -> set = A . $1; assume A2: A is Hall ; ::_thesis: ex X being set st X is_a_system_of_different_representatives_of A A3: for a being Element of dA holds F meets H1(a) proof let a be Element of dA; ::_thesis: F meets H1(a) set z = the Element of A . a; A . a <> {} by A2; then A4: the Element of A . a in A . a ; ( rng A c= bool F & A . a in rng A ) by FINSEQ_1:def_4, FUNCT_1:3; hence F meets H1(a) by A4, XBOOLE_0:3; ::_thesis: verum end; ex f being Function of dA,F st for a being Element of dA holds f . a in H1(a) from FUNCT_2:sch_10(A3); then consider f being Function of dA,F such that A5: for a being Element of dA holds f . a in H1(a) ; A6: dom f = dom A by FUNCT_2:def_1; A7: rng f c= F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F ) A8: rng A c= bool F by FINSEQ_1:def_4; assume x in rng f ; ::_thesis: x in F then consider y being set such that A9: y in dom f and A10: x = f . y by FUNCT_1:def_3; ( f . y in A . y & A . y in rng A ) by A5, A6, A9, FUNCT_1:3; hence x in F by A10, A8; ::_thesis: verum end; ex n being Nat st dom A = Seg n by FINSEQ_1:def_2; then f is FinSequence by A6, FINSEQ_1:def_2; then reconsider f = f as FinSequence of F by A7, FINSEQ_1:def_4; A11: dom A = dom f by FUNCT_2:def_1; A12: card {{}} = 1 by CARD_1:30; for i, j being Element of NAT st i in dom f & j in dom f & i <> j holds f . i <> f . j proof let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & i <> j implies f . i <> f . j ) assume that A13: i in dom f and A14: j in dom f and A15: i <> j ; ::_thesis: f . i <> f . j thus f . i <> f . j ::_thesis: verum proof card (A . i) = card {{}} by A1, A12, A11, A13; then consider y being set such that A16: A . i = {y} by CARD_1:29; A17: A . i = {(f . i)} proof thus A . i c= {(f . i)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . i)} c= A . i proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . i or x in {(f . i)} ) assume A18: x in A . i ; ::_thesis: x in {(f . i)} x = f . i proof f . i in A . i by A5, A6, A13; then A19: f . i = y by A16, TARSKI:def_1; assume x <> f . i ; ::_thesis: contradiction hence contradiction by A16, A18, A19, TARSKI:def_1; ::_thesis: verum end; hence x in {(f . i)} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(f . i)} or x in A . i ) assume x in {(f . i)} ; ::_thesis: x in A . i then x = f . i by TARSKI:def_1; hence x in A . i by A5, A6, A13; ::_thesis: verum end; A20: j in dom A by A14, FUNCT_2:def_1; then card (A . j) = card {{}} by A1, A12; then consider z being set such that A21: A . j = {z} by CARD_1:29; A22: A . j = {(f . j)} proof thus A . j c= {(f . j)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . j)} c= A . j proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . j or x in {(f . j)} ) assume A23: x in A . j ; ::_thesis: x in {(f . j)} x = f . j proof f . j in A . j by A5, A6, A14; then A24: f . j = z by A21, TARSKI:def_1; assume x <> f . j ; ::_thesis: contradiction hence contradiction by A21, A23, A24, TARSKI:def_1; ::_thesis: verum end; hence x in {(f . j)} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(f . j)} or x in A . j ) assume x in {(f . j)} ; ::_thesis: x in A . j then x = f . j by TARSKI:def_1; hence x in A . j by A5, A6, A14; ::_thesis: verum end; set J = {i,j}; assume f . i = f . j ; ::_thesis: contradiction then A25: {(f . i),(f . j)} = {(f . i)} by ENUMSET1:29; A26: card {i,j} = 2 by A15, CARD_2:57; A27: i in dom A by A13, FUNCT_2:def_1; then A28: {i,j} c= dom A by A20, ZFMISC_1:32; card (union (A,{i,j})) = card ((A . i) \/ (A . j)) by A27, A20, Th6 .= card {(f . i),(f . j)} by A17, A22, ENUMSET1:1 .= 1 by A25, CARD_1:30 ; hence contradiction by A2, A26, A28, Def4; ::_thesis: verum end; end; then for i, j being set st i in dom f & j in dom f & f . i = f . j holds i = j ; then A29: f is one-to-one by FUNCT_1:def_4; for i being Element of NAT st i in dom f holds f . i in A . i by A5, A6; then f is_a_system_of_different_representatives_of A by A11, A29, Def3; hence ex X being set st X is_a_system_of_different_representatives_of A ; ::_thesis: verum end; theorem Th18: :: HALLMAR1:18 for F being finite set for A being FinSequence of bool F st ex X being set st X is_a_system_of_different_representatives_of A holds A is Hall proof let F be finite set ; ::_thesis: for A being FinSequence of bool F st ex X being set st X is_a_system_of_different_representatives_of A holds A is Hall let A be FinSequence of bool F; ::_thesis: ( ex X being set st X is_a_system_of_different_representatives_of A implies A is Hall ) given X being set such that A1: X is_a_system_of_different_representatives_of A ; ::_thesis: A is Hall consider f being FinSequence of F such that f = X and A2: dom A = dom f and A3: for i being Element of NAT st i in dom f holds f . i in A . i and A4: f is one-to-one by A1, Def3; for J being finite set st J c= dom A holds card J <= card (union (A,J)) proof let J be finite set ; ::_thesis: ( J c= dom A implies card J <= card (union (A,J)) ) set X = J; set Y = union (A,J); set g = f | J; assume A5: J c= dom A ; ::_thesis: card J <= card (union (A,J)) then A6: dom (f | J) = J by A2, RELAT_1:62; A7: dom (f | J) c= dom f by RELAT_1:60; A8: rng (f | J) c= union (A,J) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f | J) or x in union (A,J) ) assume x in rng (f | J) ; ::_thesis: x in union (A,J) then consider a being set such that A9: a in dom (f | J) and A10: x = (f | J) . a by FUNCT_1:def_3; a in dom f by A7, A9; then reconsider a = a as Element of NAT ; f . a in A . a by A2, A3, A5, A6, A9; then (f | J) . a in A . a by A9, FUNCT_1:47; hence x in union (A,J) by A5, A6, A9, A10, Def1; ::_thesis: verum end; f | J is one-to-one by A4, FUNCT_1:52; then card J c= card (union (A,J)) by A6, A8, CARD_1:10; hence card J <= card (union (A,J)) by NAT_1:39; ::_thesis: verum end; hence A is Hall by Def4; ::_thesis: verum end; begin definition let F be set ; let A be FinSequence of bool F; let i be Element of NAT ; mode Reduction of A,i -> FinSequence of bool F means :Def5: :: HALLMAR1:def 5 ( dom it = dom A & ( for j being Element of NAT st j in dom A & j <> i holds A . j = it . j ) & it . i c= A . i ); existence ex b1 being FinSequence of bool F st ( dom b1 = dom A & ( for j being Element of NAT st j in dom A & j <> i holds A . j = b1 . j ) & b1 . i c= A . i ) proof take A ; ::_thesis: ( dom A = dom A & ( for j being Element of NAT st j in dom A & j <> i holds A . j = A . j ) & A . i c= A . i ) thus ( dom A = dom A & ( for j being Element of NAT st j in dom A & j <> i holds A . j = A . j ) & A . i c= A . i ) ; ::_thesis: verum end; end; :: deftheorem Def5 defines Reduction HALLMAR1:def_5_:_ for F being set for A being FinSequence of bool F for i being Element of NAT for b4 being FinSequence of bool F holds ( b4 is Reduction of A,i iff ( dom b4 = dom A & ( for j being Element of NAT st j in dom A & j <> i holds A . j = b4 . j ) & b4 . i c= A . i ) ); definition let F be set ; let A be FinSequence of bool F; mode Reduction of A -> FinSequence of bool F means :Def6: :: HALLMAR1:def 6 ( dom it = dom A & ( for i being Element of NAT st i in dom A holds it . i c= A . i ) ); existence ex b1 being FinSequence of bool F st ( dom b1 = dom A & ( for i being Element of NAT st i in dom A holds b1 . i c= A . i ) ) proof for i being Element of NAT st i in dom A holds A . i c= A . i ; hence ex b1 being FinSequence of bool F st ( dom b1 = dom A & ( for i being Element of NAT st i in dom A holds b1 . i c= A . i ) ) ; ::_thesis: verum end; end; :: deftheorem Def6 defines Reduction HALLMAR1:def_6_:_ for F being set for A, b3 being FinSequence of bool F holds ( b3 is Reduction of A iff ( dom b3 = dom A & ( for i being Element of NAT st i in dom A holds b3 . i c= A . i ) ) ); definition let F be set ; let A be FinSequence of bool F; let i be Element of NAT ; assume that A1: i in dom A and A2: A . i <> {} ; mode Singlification of A,i -> Reduction of A means :Def7: :: HALLMAR1:def 7 card (it . i) = 1; existence ex b1 being Reduction of A st card (b1 . i) = 1 proof set x = the Element of A . i; ( A . i in bool F & the Element of A . i in A . i ) by A1, A2, PARTFUN1:4; then reconsider E = { the Element of A . i} as Subset of F by ZFMISC_1:31; reconsider G = A +* (i,E) as FinSequence of bool F ; A3: for j being Element of NAT st j in dom A holds G . j c= A . j proof let j be Element of NAT ; ::_thesis: ( j in dom A implies G . j c= A . j ) assume j in dom A ; ::_thesis: G . j c= A . j percases ( j = i or j <> i ) ; supposeA4: j = i ; ::_thesis: G . j c= A . j G . i = { the Element of A . i} by A1, FUNCT_7:31; hence G . j c= A . j by A2, A4, ZFMISC_1:31; ::_thesis: verum end; suppose j <> i ; ::_thesis: G . j c= A . j hence G . j c= A . j by FUNCT_7:32; ::_thesis: verum end; end; end; G . i = { the Element of A . i} by A1, FUNCT_7:31; then A5: card (G . i) = 1 by CARD_2:42; dom G = dom A by FUNCT_7:30; then G is Reduction of A by A3, Def6; hence ex b1 being Reduction of A st card (b1 . i) = 1 by A5; ::_thesis: verum end; end; :: deftheorem Def7 defines Singlification HALLMAR1:def_7_:_ for F being set for A being FinSequence of bool F for i being Element of NAT st i in dom A & A . i <> {} holds for b4 being Reduction of A holds ( b4 is Singlification of A,i iff card (b4 . i) = 1 ); theorem Th19: :: HALLMAR1:19 for F being finite set for A being FinSequence of bool F for i being Element of NAT for C being Reduction of A,i holds C is Reduction of A proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT for C being Reduction of A,i holds C is Reduction of A let A be FinSequence of bool F; ::_thesis: for i being Element of NAT for C being Reduction of A,i holds C is Reduction of A let i be Element of NAT ; ::_thesis: for C being Reduction of A,i holds C is Reduction of A let C be Reduction of A,i; ::_thesis: C is Reduction of A A1: dom C = dom A by Def5; for j being Element of NAT st j in dom C holds C . j c= A . j proof let j be Element of NAT ; ::_thesis: ( j in dom C implies C . j c= A . j ) assume A2: j in dom C ; ::_thesis: C . j c= A . j percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: C . j c= A . j hence C . j c= A . j by Def5; ::_thesis: verum end; suppose j <> i ; ::_thesis: C . j c= A . j hence C . j c= A . j by A1, A2, Def5; ::_thesis: verum end; end; end; hence C is Reduction of A by A1, Def6; ::_thesis: verum end; theorem Th20: :: HALLMAR1:20 for F being finite set for A being FinSequence of bool F for i being Element of NAT for x being set st i in dom A holds Cut (A,i,x) is Reduction of A,i proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT for x being set st i in dom A holds Cut (A,i,x) is Reduction of A,i let A be FinSequence of bool F; ::_thesis: for i being Element of NAT for x being set st i in dom A holds Cut (A,i,x) is Reduction of A,i let i be Element of NAT ; ::_thesis: for x being set st i in dom A holds Cut (A,i,x) is Reduction of A,i let x be set ; ::_thesis: ( i in dom A implies Cut (A,i,x) is Reduction of A,i ) set f = Cut (A,i,x); A1: dom (Cut (A,i,x)) = dom A by Def2; then A2: for j being Element of NAT st j in dom A & j <> i holds A . j = (Cut (A,i,x)) . j by Def2; assume i in dom A ; ::_thesis: Cut (A,i,x) is Reduction of A,i then (Cut (A,i,x)) . i = (A . i) \ {x} by A1, Def2; hence Cut (A,i,x) is Reduction of A,i by A1, A2, Def5; ::_thesis: verum end; theorem Th21: :: HALLMAR1:21 for F being finite set for A being FinSequence of bool F for i being Element of NAT for x being set st i in dom A holds Cut (A,i,x) is Reduction of A proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT for x being set st i in dom A holds Cut (A,i,x) is Reduction of A let A be FinSequence of bool F; ::_thesis: for i being Element of NAT for x being set st i in dom A holds Cut (A,i,x) is Reduction of A let i be Element of NAT ; ::_thesis: for x being set st i in dom A holds Cut (A,i,x) is Reduction of A let x be set ; ::_thesis: ( i in dom A implies Cut (A,i,x) is Reduction of A ) assume i in dom A ; ::_thesis: Cut (A,i,x) is Reduction of A then Cut (A,i,x) is Reduction of A,i by Th20; hence Cut (A,i,x) is Reduction of A by Th19; ::_thesis: verum end; theorem Th22: :: HALLMAR1:22 for F being finite set for A being FinSequence of bool F for B being Reduction of A for C being Reduction of B holds C is Reduction of A proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for B being Reduction of A for C being Reduction of B holds C is Reduction of A let A be FinSequence of bool F; ::_thesis: for B being Reduction of A for C being Reduction of B holds C is Reduction of A let B be Reduction of A; ::_thesis: for C being Reduction of B holds C is Reduction of A let C be Reduction of B; ::_thesis: C is Reduction of A A1: for i being Element of NAT st i in dom A holds C . i c= A . i proof let i be Element of NAT ; ::_thesis: ( i in dom A implies C . i c= A . i ) assume A2: i in dom A ; ::_thesis: C . i c= A . i then i in dom B by Def6; then A3: C . i c= B . i by Def6; B . i c= A . i by A2, Def6; hence C . i c= A . i by A3, XBOOLE_1:1; ::_thesis: verum end; dom B = dom C by Def6; hence C is Reduction of A by A1, Def6; ::_thesis: verum end; theorem :: HALLMAR1:23 for F being non empty finite set for A being non-empty FinSequence of bool F for i being Element of NAT for B being Singlification of A,i st i in dom A holds B . i <> {} proof let F be non empty finite set ; ::_thesis: for A being non-empty FinSequence of bool F for i being Element of NAT for B being Singlification of A,i st i in dom A holds B . i <> {} let A be non-empty FinSequence of bool F; ::_thesis: for i being Element of NAT for B being Singlification of A,i st i in dom A holds B . i <> {} let i be Element of NAT ; ::_thesis: for B being Singlification of A,i st i in dom A holds B . i <> {} let B be Singlification of A,i; ::_thesis: ( i in dom A implies B . i <> {} ) assume A1: i in dom A ; ::_thesis: B . i <> {} then A . i <> {} by Th2; hence B . i <> {} by A1, Def7, CARD_1:27; ::_thesis: verum end; theorem Th24: :: HALLMAR1:24 for F being non empty finite set for A being non-empty FinSequence of bool F for i, j being Element of NAT for B being Singlification of A,i for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds ( C is Singlification of A,j & C is Singlification of A,i ) proof let F be non empty finite set ; ::_thesis: for A being non-empty FinSequence of bool F for i, j being Element of NAT for B being Singlification of A,i for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds ( C is Singlification of A,j & C is Singlification of A,i ) let A be non-empty FinSequence of bool F; ::_thesis: for i, j being Element of NAT for B being Singlification of A,i for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds ( C is Singlification of A,j & C is Singlification of A,i ) let i, j be Element of NAT ; ::_thesis: for B being Singlification of A,i for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds ( C is Singlification of A,j & C is Singlification of A,i ) let B be Singlification of A,i; ::_thesis: for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds ( C is Singlification of A,j & C is Singlification of A,i ) let C be Singlification of B,j; ::_thesis: ( i in dom A & j in dom A & C . i <> {} & B . j <> {} implies ( C is Singlification of A,j & C is Singlification of A,i ) ) assume that A1: i in dom A and A2: j in dom A and A3: C . i <> {} and A4: B . j <> {} ; ::_thesis: ( C is Singlification of A,j & C is Singlification of A,i ) A5: dom B = dom A by Def6; then A6: C . i c= B . i by A1, Def6; A7: A . i <> {} by A1, Th2; then card (B . i) = 1 by A1, Def7; then A8: card (C . i) = 1 by A3, A6, NAT_1:25, NAT_1:43; A9: A . j <> {} by A2, Th2; A10: C is Reduction of A by Th22; card (C . j) = 1 by A2, A4, A5, Def7; hence ( C is Singlification of A,j & C is Singlification of A,i ) by A1, A2, A7, A9, A10, A8, Def7; ::_thesis: verum end; theorem :: HALLMAR1:25 for F being set for A being FinSequence of bool F for i being Element of NAT holds A is Reduction of A,i proof let F be set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT holds A is Reduction of A,i let A be FinSequence of bool F; ::_thesis: for i being Element of NAT holds A is Reduction of A,i let i be Element of NAT ; ::_thesis: A is Reduction of A,i ( ( for j being Element of NAT st j in dom A & j <> i holds A . j = A . j ) & A . i c= A . i ) ; hence A is Reduction of A,i by Def5; ::_thesis: verum end; theorem Th26: :: HALLMAR1:26 for F being set for A being FinSequence of bool F holds A is Reduction of A proof let F be set ; ::_thesis: for A being FinSequence of bool F holds A is Reduction of A let A be FinSequence of bool F; ::_thesis: A is Reduction of A for i being Element of NAT st i in dom A holds A . i c= A . i ; hence A is Reduction of A by Def6; ::_thesis: verum end; definition let F be non empty set ; let A be FinSequence of bool F; assume A1: A is non-empty ; mode Singlification of A -> Reduction of A means :Def8: :: HALLMAR1:def 8 for i being Element of NAT st i in dom A holds card (it . i) = 1; existence ex b1 being Reduction of A st for i being Element of NAT st i in dom A holds card (b1 . i) = 1 proof deffunc H1( set ) -> set = {(choose (A . $1))}; A2: for x being set st x in dom A holds H1(x) in bool F proof let x be set ; ::_thesis: ( x in dom A implies H1(x) in bool F ) assume A3: x in dom A ; ::_thesis: H1(x) in bool F then A . x <> {} by A1, Th2; then A4: {(choose (A . x))} c= A . x by ZFMISC_1:31; A . x in bool F by A3, PARTFUN1:4; then {(choose (A . x))} c= F by A4, XBOOLE_1:1; hence H1(x) in bool F ; ::_thesis: verum end; ex f being Function of (dom A),(bool F) st for x being set st x in dom A holds f . x = H1(x) from FUNCT_2:sch_2(A2); then consider f being Function of (dom A),(bool F) such that A5: for x being set st x in dom A holds f . x = H1(x) ; A6: for i being Element of NAT st i in dom f holds f . i = {(choose (A . i))} proof let i be Element of NAT ; ::_thesis: ( i in dom f implies f . i = {(choose (A . i))} ) assume i in dom f ; ::_thesis: f . i = {(choose (A . i))} then i in dom A by FUNCT_2:def_1; hence f . i = {(choose (A . i))} by A5; ::_thesis: verum end; A7: dom f = dom A by FUNCT_2:def_1; A8: for i being Element of NAT st i in dom A holds f . i c= A . i proof let i be Element of NAT ; ::_thesis: ( i in dom A implies f . i c= A . i ) assume A9: i in dom A ; ::_thesis: f . i c= A . i then A . i <> {} by A1, Th2; then {(choose (A . i))} c= A . i by ZFMISC_1:31; hence f . i c= A . i by A7, A6, A9; ::_thesis: verum end; dom f = dom A by FUNCT_2:def_1 .= Seg (len A) by FINSEQ_1:def_3 ; then A10: f is FinSequence by FINSEQ_1:def_2; rng f c= bool F by RELAT_1:def_19; then f is FinSequence of bool F by A10, FINSEQ_1:def_4; then reconsider f = f as Reduction of A by A7, A8, Def6; for i being Element of NAT st i in dom A holds card (f . i) = 1 proof let i be Element of NAT ; ::_thesis: ( i in dom A implies card (f . i) = 1 ) assume i in dom A ; ::_thesis: card (f . i) = 1 then i in dom f by FUNCT_2:def_1; then f . i = {(choose (A . i))} by A6; hence card (f . i) = 1 by CARD_2:42; ::_thesis: verum end; hence ex b1 being Reduction of A st for i being Element of NAT st i in dom A holds card (b1 . i) = 1 ; ::_thesis: verum end; end; :: deftheorem Def8 defines Singlification HALLMAR1:def_8_:_ for F being non empty set for A being FinSequence of bool F st A is non-empty holds for b3 being Reduction of A holds ( b3 is Singlification of A iff for i being Element of NAT st i in dom A holds card (b3 . i) = 1 ); theorem Th27: :: HALLMAR1:27 for F being non empty finite set for A being non empty non-empty FinSequence of bool F for f being Function holds ( f is Singlification of A iff ( dom f = dom A & ( for i being Element of NAT st i in dom A holds f is Singlification of A,i ) ) ) proof let F be non empty finite set ; ::_thesis: for A being non empty non-empty FinSequence of bool F for f being Function holds ( f is Singlification of A iff ( dom f = dom A & ( for i being Element of NAT st i in dom A holds f is Singlification of A,i ) ) ) let A be non empty non-empty FinSequence of bool F; ::_thesis: for f being Function holds ( f is Singlification of A iff ( dom f = dom A & ( for i being Element of NAT st i in dom A holds f is Singlification of A,i ) ) ) let f be Function; ::_thesis: ( f is Singlification of A iff ( dom f = dom A & ( for i being Element of NAT st i in dom A holds f is Singlification of A,i ) ) ) hereby ::_thesis: ( dom f = dom A & ( for i being Element of NAT st i in dom A holds f is Singlification of A,i ) implies f is Singlification of A ) assume f is Singlification of A ; ::_thesis: ( dom f = dom A & ( for i being Element of NAT st i in dom A holds f is Singlification of A,i ) ) then reconsider f9 = f as Singlification of A ; f9 is Reduction of A ; hence dom f = dom A by Def6; ::_thesis: for i being Element of NAT st i in dom A holds f is Singlification of A,i let i be Element of NAT ; ::_thesis: ( i in dom A implies f is Singlification of A,i ) assume A1: i in dom A ; ::_thesis: f is Singlification of A,i then ( card (f9 . i) = 1 & A . i <> {} ) by Def8; hence f is Singlification of A,i by A1, Def7; ::_thesis: verum end; assume that A2: dom f = dom A and A3: for i being Element of NAT st i in dom A holds f is Singlification of A,i ; ::_thesis: f is Singlification of A reconsider f = f as FinSequence of bool F by A3, FINSEQ_5:6; for i being Element of NAT st i in dom A holds f . i c= A . i proof let i be Element of NAT ; ::_thesis: ( i in dom A implies f . i c= A . i ) assume A4: i in dom A ; ::_thesis: f . i c= A . i then f is Singlification of A,i by A3; hence f . i c= A . i by A4, Def6; ::_thesis: verum end; then reconsider f9 = f as Reduction of A by A2, Def6; for i being Element of NAT st i in dom A holds card (f9 . i) = 1 proof let i be Element of NAT ; ::_thesis: ( i in dom A implies card (f9 . i) = 1 ) assume A5: i in dom A ; ::_thesis: card (f9 . i) = 1 then ( f is Singlification of A,i & A . i <> {} ) by A3; hence card (f9 . i) = 1 by A5, Def7; ::_thesis: verum end; hence f is Singlification of A by Def8; ::_thesis: verum end; registration let F be non empty finite set ; let A be non empty FinSequence of bool F; let k be Element of NAT ; cluster -> non empty for Singlification of A,k; coherence for b1 being Singlification of A,k holds not b1 is empty proof let G be Singlification of A,k; ::_thesis: not G is empty dom G = dom A by Def6; hence not G is empty ; ::_thesis: verum end; end; registration let F be non empty finite set ; let A be non empty FinSequence of bool F; cluster -> non empty for Singlification of A; coherence for b1 being Singlification of A holds not b1 is empty proof let G be Singlification of A; ::_thesis: not G is empty dom G = dom A by Def6; hence not G is empty ; ::_thesis: verum end; end; begin theorem Th28: :: HALLMAR1:28 for F being non empty finite set for A being non empty FinSequence of bool F for X being set for B being Reduction of A st X is_a_system_of_different_representatives_of B holds X is_a_system_of_different_representatives_of A proof let F be non empty finite set ; ::_thesis: for A being non empty FinSequence of bool F for X being set for B being Reduction of A st X is_a_system_of_different_representatives_of B holds X is_a_system_of_different_representatives_of A let A be non empty FinSequence of bool F; ::_thesis: for X being set for B being Reduction of A st X is_a_system_of_different_representatives_of B holds X is_a_system_of_different_representatives_of A let X be set ; ::_thesis: for B being Reduction of A st X is_a_system_of_different_representatives_of B holds X is_a_system_of_different_representatives_of A let B be Reduction of A; ::_thesis: ( X is_a_system_of_different_representatives_of B implies X is_a_system_of_different_representatives_of A ) assume A1: X is_a_system_of_different_representatives_of B ; ::_thesis: X is_a_system_of_different_representatives_of A X is_a_system_of_different_representatives_of A proof consider f being FinSequence of F such that A2: f = X and A3: dom B = dom f and A4: for i being Element of NAT st i in dom f holds f . i in B . i and A5: f is one-to-one by A1, Def3; A6: for i being Element of NAT st i in dom f holds f . i in A . i proof let i be Element of NAT ; ::_thesis: ( i in dom f implies f . i in A . i ) assume A7: i in dom f ; ::_thesis: f . i in A . i A8: f . i in B . i by A4, A7; dom B = dom A by Def6; then B . i c= A . i by A3, A7, Def6; hence f . i in A . i by A8; ::_thesis: verum end; dom A = dom B by Def6; hence X is_a_system_of_different_representatives_of A by A2, A3, A5, A6, Def3; ::_thesis: verum end; hence X is_a_system_of_different_representatives_of A ; ::_thesis: verum end; theorem Th29: :: HALLMAR1:29 for F being finite set for A being FinSequence of bool F st A is Hall holds for i being Element of NAT st card (A . i) >= 2 holds ex x being set st ( x in A . i & Cut (A,i,x) is Hall ) proof let F be finite set ; ::_thesis: for A being FinSequence of bool F st A is Hall holds for i being Element of NAT st card (A . i) >= 2 holds ex x being set st ( x in A . i & Cut (A,i,x) is Hall ) let A be FinSequence of bool F; ::_thesis: ( A is Hall implies for i being Element of NAT st card (A . i) >= 2 holds ex x being set st ( x in A . i & Cut (A,i,x) is Hall ) ) assume A1: A is Hall ; ::_thesis: for i being Element of NAT st card (A . i) >= 2 holds ex x being set st ( x in A . i & Cut (A,i,x) is Hall ) let i be Element of NAT ; ::_thesis: ( card (A . i) >= 2 implies ex x being set st ( x in A . i & Cut (A,i,x) is Hall ) ) assume A2: card (A . i) >= 2 ; ::_thesis: ex x being set st ( x in A . i & Cut (A,i,x) is Hall ) 2 c= card (A . i) by A2, NAT_1:39; then reconsider Ai = A . i as non trivial finite set by PENCIL_1:4; consider x, y being set such that A3: x in Ai and A4: y in Ai and A5: x <> y by ZFMISC_1:def_10; assume A6: for z being set st z in A . i holds not Cut (A,i,z) is Hall ; ::_thesis: contradiction then not Cut (A,i,x) is Hall by A3; then consider JJ1 being finite set such that A7: JJ1 c= dom (Cut (A,i,x)) and A8: card JJ1 > card (union ((Cut (A,i,x)),JJ1)) by Def4; ex J1 being finite set st ( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) proof percases ( i in JJ1 or not i in JJ1 ) ; supposeA9: i in JJ1 ; ::_thesis: ex J1 being finite set st ( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) set J1 = JJ1 \ {i}; A10: card (JJ1 \ {i}) = (card JJ1) - (card {i}) by A9, EULER_1:4 .= (card JJ1) - 1 by CARD_1:30 ; A11: ( JJ1 \ {i} c= dom (Cut (A,i,x)) & {i} misses JJ1 \ {i} ) by A7, XBOOLE_1:1, XBOOLE_1:79; union ((Cut (A,i,x)),JJ1) = (union (A,(JJ1 \ {i}))) \/ ((A . i) \ {x}) by A7, A9, Th14; then card (JJ1 \ {i}) >= card ((union (A,(JJ1 \ {i}))) \/ ((A . i) \ {x})) by A8, A10, SPPOL_1:1; hence ex J1 being finite set st ( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) by A11, ZFMISC_1:48; ::_thesis: verum end; supposeA12: not i in JJ1 ; ::_thesis: ex J1 being finite set st ( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) take J1 = JJ1; ::_thesis: ( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) A13: J1 c= dom A by A7, Def2; card J1 > card (union (A,J1)) by A8, A12, Th13; hence ( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) by A1, A13, Def4; ::_thesis: verum end; end; end; then consider J1 being finite set such that A14: not i in J1 and A15: J1 c= dom (Cut (A,i,x)) and A16: card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ; not Cut (A,i,y) is Hall by A4, A6; then consider JJ2 being finite set such that A17: JJ2 c= dom (Cut (A,i,y)) and A18: card JJ2 > card (union ((Cut (A,i,y)),JJ2)) by Def4; ex J2 being finite set st ( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) ) proof percases ( i in JJ2 or not i in JJ2 ) ; supposeA19: i in JJ2 ; ::_thesis: ex J2 being finite set st ( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) ) set J2 = JJ2 \ {i}; A20: card (JJ2 \ {i}) = (card JJ2) - (card {i}) by A19, EULER_1:4 .= (card JJ2) - 1 by CARD_1:30 ; A21: ( JJ2 \ {i} c= dom (Cut (A,i,y)) & {i} misses JJ2 \ {i} ) by A17, XBOOLE_1:1, XBOOLE_1:79; union ((Cut (A,i,y)),JJ2) = (union (A,(JJ2 \ {i}))) \/ ((A . i) \ {y}) by A17, A19, Th14; then card (JJ2 \ {i}) >= card ((union (A,(JJ2 \ {i}))) \/ ((A . i) \ {y})) by A18, A20, SPPOL_1:1; hence ex J2 being finite set st ( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) ) by A21, ZFMISC_1:48; ::_thesis: verum end; supposeA22: not i in JJ2 ; ::_thesis: ex J2 being finite set st ( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) ) set J2 = JJ2; take JJ2 ; ::_thesis: ( not i in JJ2 & JJ2 c= dom (Cut (A,i,y)) & card JJ2 >= card ((union (A,JJ2)) \/ ((A . i) \ {y})) ) A23: JJ2 c= dom A by A17, Def2; card JJ2 > card (union (A,JJ2)) by A18, A22, Th13; hence ( not i in JJ2 & JJ2 c= dom (Cut (A,i,y)) & card JJ2 >= card ((union (A,JJ2)) \/ ((A . i) \ {y})) ) by A1, A23, Def4; ::_thesis: verum end; end; end; then consider J2 being finite set such that A24: not i in J2 and A25: J2 c= dom (Cut (A,i,y)) and A26: card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) ; reconsider L = {i} \/ (J1 \/ J2) as finite set ; A27: J2 c= dom A by A25, Def2; (union (A,(J1 \/ J2))) \/ Ai c= ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union (A,(J1 \/ J2))) \/ Ai or a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) ) assume A28: a in (union (A,(J1 \/ J2))) \/ Ai ; ::_thesis: a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) percases ( a in union (A,(J1 \/ J2)) or a in Ai ) by A28, XBOOLE_0:def_3; suppose a in union (A,(J1 \/ J2)) ; ::_thesis: a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) then consider j being set such that A29: j in J1 \/ J2 and A30: ( j in dom A & a in A . j ) by Def1; ( j in J1 or j in J2 ) by A29, XBOOLE_0:def_3; then ( a in union (A,J1) or a in union (A,J2) ) by A30, Def1; then a in (union (A,J1)) \/ (union (A,J2)) by XBOOLE_0:def_3; then a in ((union (A,J1)) \/ (union (A,J2))) \/ ((Ai \ {x}) \/ (Ai \ {y})) by XBOOLE_0:def_3; then a in (((union (A,J1)) \/ (union (A,J2))) \/ (Ai \ {x})) \/ (Ai \ {y}) by XBOOLE_1:4; then a in (((union (A,J1)) \/ (Ai \ {x})) \/ (union (A,J2))) \/ (Ai \ {y}) by XBOOLE_1:4; hence a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) by XBOOLE_1:4; ::_thesis: verum end; suppose a in Ai ; ::_thesis: a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) then ( a in (Ai \ {x}) \/ (Ai \ {y}) or a in union (A,J1) or a in union (A,J2) ) by A3, A4, A5, Th10; then ( a in ((Ai \ {x}) \/ (Ai \ {y})) \/ (union (A,J1)) or a in union (A,J2) ) by XBOOLE_0:def_3; then a in (((Ai \ {x}) \/ (Ai \ {y})) \/ (union (A,J1))) \/ (union (A,J2)) by XBOOLE_0:def_3; then a in ((union (A,J1)) \/ (union (A,J2))) \/ ((Ai \ {x}) \/ (Ai \ {y})) by XBOOLE_1:4; then a in (((union (A,J1)) \/ (union (A,J2))) \/ (Ai \ {x})) \/ (Ai \ {y}) by XBOOLE_1:4; then a in (((union (A,J1)) \/ (Ai \ {x})) \/ (union (A,J2))) \/ (Ai \ {y}) by XBOOLE_1:4; hence a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) by XBOOLE_1:4; ::_thesis: verum end; end; end; then A31: card (((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y}))) >= card ((union (A,(J1 \/ J2))) \/ Ai) by NAT_1:43; union (A,(J1 /\ J2)) c= (union (A,J1)) /\ (union (A,J2)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,(J1 /\ J2)) or x in (union (A,J1)) /\ (union (A,J2)) ) assume x in union (A,(J1 /\ J2)) ; ::_thesis: x in (union (A,J1)) /\ (union (A,J2)) then consider j being set such that A32: j in J1 /\ J2 and A33: ( j in dom A & x in A . j ) by Def1; j in J2 by A32, XBOOLE_0:def_4; then A34: x in union (A,J2) by A33, Def1; j in J1 by A32, XBOOLE_0:def_4; then x in union (A,J1) by A33, Def1; hence x in (union (A,J1)) /\ (union (A,J2)) by A34, XBOOLE_0:def_4; ::_thesis: verum end; then card ((union (A,J1)) /\ (union (A,J2))) >= card (union (A,(J1 /\ J2))) by NAT_1:43; then A35: (card ((union (A,(J1 \/ J2))) \/ Ai)) + (card ((union (A,J1)) /\ (union (A,J2)))) >= (card (Ai \/ (union (A,(J1 \/ J2))))) + (card (union (A,(J1 /\ J2)))) by XREAL_1:7; J1 c= dom A by A15, Def2; then A36: J1 \/ J2 c= dom A by A27, XBOOLE_1:8; A37: i in dom A by A2, CARD_1:27, FUNCT_1:def_2; then {i} c= dom A by ZFMISC_1:31; then L c= dom A by A36, XBOOLE_1:8; then card (union (A,({i} \/ (J1 \/ J2)))) >= card ({i} \/ (J1 \/ J2)) by A1, Def4; then A38: card (union (A,(({i} \/ J1) \/ J2))) >= card ({i} \/ (J1 \/ J2)) by XBOOLE_1:4; not i in J1 \/ J2 by A14, A24, XBOOLE_0:def_3; then A39: card ({i} \/ (J1 \/ J2)) = (card {i}) + (card (J1 \/ J2)) by CARD_2:40, ZFMISC_1:50; ( J1 /\ J2 c= J1 & J1 c= dom A ) by A15, Def2, XBOOLE_1:17; then J1 /\ J2 c= dom A by XBOOLE_1:1; then A40: card (union (A,(J1 /\ J2))) >= card (J1 /\ J2) by A1, Def4; set S2 = (union (A,J2)) \/ ((A . i) \ {y}); set S1 = (union (A,J1)) \/ ((A . i) \ {x}); (card J1) + (card J2) >= (card ((union (A,J1)) \/ ((A . i) \ {x}))) + (card ((union (A,J2)) \/ ((A . i) \ {y}))) by A16, A26, XREAL_1:7; then A41: (card J1) + (card J2) >= (card (((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})))) + (card (((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})))) by Th1; (union (A,J1)) /\ (union (A,J2)) c= ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union (A,J1)) /\ (union (A,J2)) or a in ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})) ) assume A42: a in (union (A,J1)) /\ (union (A,J2)) ; ::_thesis: a in ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})) then a in union (A,J2) by XBOOLE_0:def_4; then A43: a in (union (A,J2)) \/ (Ai \ {y}) by XBOOLE_0:def_3; a in union (A,J1) by A42, XBOOLE_0:def_4; then a in (union (A,J1)) \/ (Ai \ {x}) by XBOOLE_0:def_3; hence a in ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})) by A43, XBOOLE_0:def_4; ::_thesis: verum end; then card (((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y}))) >= card ((union (A,J1)) /\ (union (A,J2))) by NAT_1:43; then (card (((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})))) + (card (((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})))) >= (card ((union (A,(J1 \/ J2))) \/ Ai)) + (card ((union (A,J1)) /\ (union (A,J2)))) by A31, XREAL_1:7; then (card J1) + (card J2) >= (card ((union (A,(J1 \/ J2))) \/ Ai)) + (card ((union (A,J1)) /\ (union (A,J2)))) by A41, XXREAL_0:2; then A44: (card J1) + (card J2) >= (card (Ai \/ (union (A,(J1 \/ J2))))) + (card (union (A,(J1 /\ J2)))) by A35, XXREAL_0:2; card (union (A,(({i} \/ J1) \/ J2))) = card (Ai \/ (union (A,(J1 \/ J2)))) by A37, Th9; then card (Ai \/ (union (A,(J1 \/ J2)))) >= 1 + (card (J1 \/ J2)) by A38, A39, CARD_1:30; then A45: (card (Ai \/ (union (A,(J1 \/ J2))))) + (card (union (A,(J1 /\ J2)))) >= (1 + (card (J1 \/ J2))) + (card (J1 /\ J2)) by A40, XREAL_1:7; (card (J1 \/ J2)) + (card (J1 /\ J2)) = (card J1) + (card J2) by Th1; then (1 + (card (J1 \/ J2))) + (card (J1 /\ J2)) = 1 + ((card J1) + (card J2)) ; hence contradiction by A44, A45, NAT_1:13; ::_thesis: verum end; theorem Th30: :: HALLMAR1:30 for F being finite set for A being FinSequence of bool F for i being Element of NAT st i in dom A & A is Hall holds ex G being Singlification of A,i st G is Hall proof let F be finite set ; ::_thesis: for A being FinSequence of bool F for i being Element of NAT st i in dom A & A is Hall holds ex G being Singlification of A,i st G is Hall let A be FinSequence of bool F; ::_thesis: for i being Element of NAT st i in dom A & A is Hall holds ex G being Singlification of A,i st G is Hall let i be Element of NAT ; ::_thesis: ( i in dom A & A is Hall implies ex G being Singlification of A,i st G is Hall ) assume that A1: i in dom A and A2: A is Hall ; ::_thesis: ex G being Singlification of A,i st G is Hall A3: A . i <> {} by A1, A2, Th16, CARD_1:27; set n = card (A . i); A4: card (A . i) >= 1 by A1, A2, Th16; defpred S1[ Element of NAT ] means ex G being Reduction of A st ( G is Hall & card (G . i) = $1 ); A5: A is Reduction of A by Th26; percases ( card (A . i) = 1 or card (A . i) > 1 ) by A4, XXREAL_0:1; suppose card (A . i) = 1 ; ::_thesis: ex G being Singlification of A,i st G is Hall then A is Singlification of A,i by A1, A5, Def7, CARD_1:27; hence ex G being Singlification of A,i st G is Hall by A2; ::_thesis: verum end; supposeA6: card (A . i) > 1 ; ::_thesis: ex G being Singlification of A,i st G is Hall A7: for k being Element of NAT st k >= 1 & S1[k + 1] holds S1[k] proof let k be Element of NAT ; ::_thesis: ( k >= 1 & S1[k + 1] implies S1[k] ) assume that A8: k >= 1 and A9: S1[k + 1] ; ::_thesis: S1[k] consider G being Reduction of A such that A10: G is Hall and A11: card (G . i) = k + 1 by A9; 1 + 1 <= k + 1 by A8, XREAL_1:6; then consider x being set such that A12: x in G . i and A13: Cut (G,i,x) is Hall by A10, A11, Th29; set H = Cut (G,i,x); A14: dom G = dom A by Def6; then Cut (G,i,x) is Reduction of G by A1, Th21; then A15: Cut (G,i,x) is Reduction of A by Th22; card ((Cut (G,i,x)) . i) = (k + 1) - 1 by A1, A11, A14, A12, Th11 .= k ; hence S1[k] by A13, A15; ::_thesis: verum end; A is Reduction of A by Th26; then A16: ex n being Element of NAT st ( n > 1 & S1[n] ) by A2, A6; S1[1] from HALLMAR1:sch_2(A16, A7); then consider G being Reduction of A such that A17: G is Hall and A18: card (G . i) = 1 ; G is Singlification of A,i by A1, A3, A18, Def7; hence ex G being Singlification of A,i st G is Hall by A17; ::_thesis: verum end; end; end; theorem Th31: :: HALLMAR1:31 for F being non empty finite set for A being non empty FinSequence of bool F st A is Hall holds ex G being Singlification of A st G is Hall proof let F be non empty finite set ; ::_thesis: for A being non empty FinSequence of bool F st A is Hall holds ex G being Singlification of A st G is Hall let A be non empty FinSequence of bool F; ::_thesis: ( A is Hall implies ex G being Singlification of A st G is Hall ) defpred S1[ Element of NAT ] means ( $1 in dom A implies ex g being Singlification of A,$1 st ( g is Hall & ( for k being Element of NAT st 1 <= k & k <= $1 holds g is Singlification of A,k ) ) ); assume A1: A is Hall ; ::_thesis: ex G being Singlification of A st G is Hall then A2: A is non-empty ; A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] ( k + 1 in dom A implies ex g being Singlification of A,k + 1 st ( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds g is Singlification of A,l ) ) ) proof assume A5: k + 1 in dom A ; ::_thesis: ex g being Singlification of A,k + 1 st ( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds g is Singlification of A,l ) ) percases ( k = 0 or k in dom A ) by A5, TAXONOM1:1; supposeA6: k = 0 ; ::_thesis: ex g being Singlification of A,k + 1 st ( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds g is Singlification of A,l ) ) consider g being Singlification of A,k + 1 such that A7: g is Hall by A1, A5, Th30; for l being Element of NAT st 1 <= l & l <= k + 1 holds g is Singlification of A,l by A6, XXREAL_0:1; hence ex g being Singlification of A,k + 1 st ( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds g is Singlification of A,l ) ) by A7; ::_thesis: verum end; supposeA8: k in dom A ; ::_thesis: ex g being Singlification of A,k + 1 st ( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds g is Singlification of A,l ) ) then consider g being Singlification of A,k such that A9: g is Hall and A10: for l being Element of NAT st 1 <= l & l <= k holds g is Singlification of A,l by A4; k + 1 in dom g by A5, Def6; then consider G being Singlification of g,k + 1 such that A11: G is Hall by A9, Th30; A12: dom g = dom A by Def6; then A13: dom G = dom A by Def6; then A14: G . k <> {} by A8, A11; A15: g . (k + 1) <> {} by A9, A5, A12; then reconsider G = G as Singlification of A,k + 1 by A2, A5, A8, A14, Th24; for l being Element of NAT st 1 <= l & l <= k + 1 holds G is Singlification of A,l proof let l be Element of NAT ; ::_thesis: ( 1 <= l & l <= k + 1 implies G is Singlification of A,l ) assume that A16: 1 <= l and A17: l <= k + 1 ; ::_thesis: G is Singlification of A,l k + 1 <= len A by A5, FINSEQ_3:25; then l <= len A by A17, XXREAL_0:2; then A18: l in dom A by A16, FINSEQ_3:25; then A19: G . l <> {} by A13, A11; percases ( l <= k or l = k + 1 ) by A17, NAT_1:8; suppose l <= k ; ::_thesis: G is Singlification of A,l then g is Singlification of A,l by A10, A16; hence G is Singlification of A,l by A2, A5, A15, A18, A19, Th24; ::_thesis: verum end; suppose l = k + 1 ; ::_thesis: G is Singlification of A,l hence G is Singlification of A,l ; ::_thesis: verum end; end; end; hence ex g being Singlification of A,k + 1 st ( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds g is Singlification of A,l ) ) by A11; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A20: S1[ 0 ] proof assume 0 in dom A ; ::_thesis: ex g being Singlification of A, 0 st ( g is Hall & ( for k being Element of NAT st 1 <= k & k <= 0 holds g is Singlification of A,k ) ) then consider G being Singlification of A, 0 such that A21: G is Hall by A1, Th30; for k being Element of NAT st 1 <= k & k <= 0 holds G is Singlification of A,k ; hence ex g being Singlification of A, 0 st ( g is Hall & ( for k being Element of NAT st 1 <= k & k <= 0 holds g is Singlification of A,k ) ) by A21; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A20, A3); then ( len A in dom A implies ex g being Singlification of A, len A st ( g is Hall & ( for l being Element of NAT st 1 <= l & l <= len A holds g is Singlification of A,l ) ) ) ; then consider G being Singlification of A, len A such that A22: G is Hall and A23: for l being Element of NAT st 1 <= l & l <= len A holds G is Singlification of A,l by FINSEQ_5:6; A24: for i being Element of NAT st i in dom A holds G is Singlification of A,i proof let i be Element of NAT ; ::_thesis: ( i in dom A implies G is Singlification of A,i ) assume i in dom A ; ::_thesis: G is Singlification of A,i then ( 1 <= i & i <= len A ) by FINSEQ_3:25; hence G is Singlification of A,i by A23; ::_thesis: verum end; dom G = dom A by Def6; then G is Singlification of A by A2, A24, Th27; hence ex G being Singlification of A st G is Hall by A22; ::_thesis: verum end; theorem :: HALLMAR1:32 for F being non empty finite set for A being non empty FinSequence of bool F holds ( ex X being set st X is_a_system_of_different_representatives_of A iff A is Hall ) proof let F be non empty finite set ; ::_thesis: for A being non empty FinSequence of bool F holds ( ex X being set st X is_a_system_of_different_representatives_of A iff A is Hall ) let A be non empty FinSequence of bool F; ::_thesis: ( ex X being set st X is_a_system_of_different_representatives_of A iff A is Hall ) thus ( ex X being set st X is_a_system_of_different_representatives_of A implies A is Hall ) by Th18; ::_thesis: ( A is Hall implies ex X being set st X is_a_system_of_different_representatives_of A ) assume A1: A is Hall ; ::_thesis: ex X being set st X is_a_system_of_different_representatives_of A then consider G being Singlification of A such that A2: G is Hall by Th31; for i being Element of NAT st i in dom G holds card (G . i) = 1 proof let i be Element of NAT ; ::_thesis: ( i in dom G implies card (G . i) = 1 ) assume A3: i in dom G ; ::_thesis: card (G . i) = 1 dom G = dom A by Def6; hence card (G . i) = 1 by A1, A3, Def8; ::_thesis: verum end; then ex X being set st X is_a_system_of_different_representatives_of G by A2, Th17; hence ex X being set st X is_a_system_of_different_representatives_of A by Th28; ::_thesis: verum end;