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 A1: f is Hall ;
take f ; :: thesis: f is Hall
thus f is Hall by A1; :: thesis: verum