per cases ( not F is empty or F is empty ) ;

suppose not F is empty ; :: thesis: ex b₁ being FinSequence of bool F st b₁ is Hall

then reconsider F1 = F as non empty finite set ;
consider f being Hall FinSequence of bool F1;
reconsider f1 = f as FinSequence of bool F ;
take f1 ; :: thesis: f1 is Hall
thus f1 is Hall ; :: thesis: verum

end;

suppose F is empty ; :: thesis: ex b₁ being FinSequence of bool F st b₁ is Hall

then reconsider b = {} as Element of bool F by TARSKI:def 1, ZFMISC_1:1;
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 A5: f is Hall by Def4;
take f ; :: thesis: f is Hall
thus f is Hall by A5; :: thesis: verum

end;

end;