set c = the Element of F;
reconsider b = { the Element of F} as Element of bool F by ZFMISC_1:37;
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))
A3: dom f = {1} by FINSEQ_1:4, FINSEQ_1:55;
then A2: ( J = {} or J = {1} ) by A1, ZFMISC_1:39;

per cases ( J = {} or J = {1} ) by A2;

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 B1: J = {1} ; :: thesis: card J <= card (union (f,J))

( 1 in dom f & 1 in NAT ) by A3, TARSKI:def 1;
then union (f,{1}) = f . 1 by Th5
.= b by FINSEQ_1:57 ;
then card (union (f,J)) = 1 by B1, CARD_1:50;
hence card J <= card (union (f,J)) by B1, CARD_1:50; :: thesis: verum

end;

end;

end;

then f is Hall by Def4;
hence ex b₁ being FinSequence of bool F st
( b₁ is Hall & not b₁ is empty ) ; :: thesis: verum