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 H₁( 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 H₁(a)

proof

let a be Element of dA; :: thesis: F meets H₁(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 H₁(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 H₁(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 H₁(a) ;
A6: dom f = dom A by FUNCT_2:def 1;
A7: rng f c= F

proof

let x be object ; :: 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 object 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 object 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 object ; :: 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 object ; :: 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 object 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 object ; :: 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 object ; :: 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; :: thesis: 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 ; :: thesis: verum