let F be 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
let A be non empty FinSequence of bool F; ( ( 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
; ( 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
; 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)
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
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 ;
( 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
;
f . i <> f . j
thus
f . i <> f . j
verumproof
card (A . i) = card {{}}
by A1, A12, A11, A13;
then consider y being
object such that A16:
A . i = {y}
by CARD_1:29;
A17:
A . i = {(f . i)}
A20:
j in dom A
by A14, FUNCT_2:def 1;
then
card (A . j) = card {{}}
by A1, A12;
then consider z being
object such that A21:
A . j = {z}
by CARD_1:29;
A22:
A . j = {(f . j)}
set J =
{i,j};
assume
f . i = f . j
;
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;
verum
end;
end;
then
for i, j being object 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;
hence
ex X being set st X is_a_system_of_different_representatives_of A
; verum