let F be non empty finite set ; :: thesis:
let A be non empty FinSequence of bool F; :: thesis:
assume A1: for i being Element of NAT st i in dom A holds
card (A . i) = 1 ; :: thesis:
assume A2: A is Hall ; :: thesis:
A3: card {{} } = 1 by CARD_1:50;
reconsider dA = dom A as non empty set ;
deffunc H₁( Element of dA) -> set = A . $1;
A4: for a being Element of dA holds F meets H₁(a)

proof

let a be Element of dA; :: thesis:
A5: rng A c= bool F by FINSEQ_1:def 4;
A6: A . a in rng A by FUNCT_1:12;
consider z being Element of A . a;
A is non-empty by A2, Th15;
then A . a <> {} ;
then z in A . a ;
hence F meets H₁(a) by A5, A6, XBOOLE_0:3; :: thesis:

end;

ex f being Function of dA,F st
for a being Element of dA holds f . a in H₁(a) from FUNCT_2:sch 11(A4);
then consider f being Function of dA,F such that
A7: for a being Element of dA holds f . a in H₁(a) ;
A8: dom f = dom A by FUNCT_2:def 1;
consider n being Nat such that
A9: dom A = Seg n by FINSEQ_1:def 2;
A10: f is FinSequence by A8, A9, FINSEQ_1:def 2;
rng f c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being set such that
A11: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
A12: f . y in A . y by A7, A8, A11;
A13: A . y in rng A by A8, A11, FUNCT_1:12;
rng A c= bool F by FINSEQ_1:def 4;
hence x in F by A11, A12, A13; :: thesis:

end;

then reconsider f = f as FinSequence of F by A10, FINSEQ_1:def 4;
A14: dom A = dom f by FUNCT_2:def 1;
A15: for i being Element of NAT st i in dom f holds
f . i in A . i by A7, A8;
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:
assume A16: ( i in dom f & j in dom f & i <> j ) ; :: thesis:
thus f . i <> f . j :: thesis:

proof

assume A17: f . i = f . j ; :: thesis:
set J = {i,j};
A18: card {i,j} = 2 by A16, CARD_2:76;
A19: ( i in dom A & j in dom A ) by A16, FUNCT_2:def 1;
then A20: {i,j} c= dom A by ZFMISC_1:38;
card (A . i) = card {{} } by A1, A3, A14, A16;
then consider y being set such that
A21: A . i = {y} by CARD_1:49;
card (A . j) = card {{} } by A1, A3, A19;
then consider z being set such that
A22: A . j = {z} by CARD_1:49;
A23: A . i = {(f . i)}

proof

thus A . i c= {(f . i)} :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A24: x in A . i ; :: thesis:
x = f . i

proof

assume A25: x <> f . i ; :: thesis:
f . i in A . i by A7, A8, A16;
then f . i = y by A21, TARSKI:def 1;
hence contradiction by A21, A24, A25, TARSKI:def 1; :: thesis:

end;

hence x in {(f . i)} by TARSKI:def 1; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {(f . i)} ; :: thesis:
then x = f . i by TARSKI:def 1;
hence x in A . i by A7, A8, A16; :: thesis:

end;

A26: A . j = {(f . j)}

proof

thus A . j c= {(f . j)} :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A27: x in A . j ; :: thesis:
x = f . j

proof

assume A28: x <> f . j ; :: thesis:
f . j in A . j by A7, A8, A16;
then f . j = z by A22, TARSKI:def 1;
hence contradiction by A22, A27, A28, TARSKI:def 1; :: thesis:

end;

hence x in {(f . j)} by TARSKI:def 1; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {(f . j)} ; :: thesis:
then x = f . j by TARSKI:def 1;
hence x in A . j by A7, A8, A16; :: thesis:

end;

A29: {(f . i),(f . j)} = {(f . i)} by A17, ENUMSET1:69;
card (union A,{i,j}) = card ((A . i) \/ (A . j)) by A19, Th6
.= card {(f . i),(f . j)} by A23, A26, ENUMSET1:41
.= 1 by A29, CARD_1:50 ;
hence contradiction by A2, A18, A20, Def4; :: thesis:

end;

then for i, j being set st i in dom f & j in dom f & f . i = f . j holds
i = j ;
then f is one-to-one by FUNCT_1:def 8;
then f is_a_system_of_different_representatives_of A by A14, A15, Def3;
hence ex X being set st X is_a_system_of_different_representatives_of A ; :: thesis: