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;

per cases ( 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;

suppose A4: 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 ;
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 ;
hence ex b₁ being FinSequence of bool F st
( b₁ is Hall & not b₁ is empty ) ; :: thesis: verum