let F be finite set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT st i in dom A & A is Hall holds
card (A . i) >= 1
let A be FinSequence of bool F; :: thesis: for i being Element of NAT st i in dom A & A is Hall holds
card (A . i) >= 1
let i be Element of NAT ; :: thesis: ( i in dom A & A is Hall implies card (A . i) >= 1 )
assume A1: ( i in dom A & A is Hall ) ; :: thesis: card (A . i) >= 1
assume A2: card (A . i) < 1 ; :: thesis: contradiction
set J = {i};
A3: union A,{i} = A . i by A1, Th5;
{i} c= dom A by A1, ZFMISC_1:37;
then card {i} <= card (union A,{i}) by A1, Def4;
hence contradiction by A2, A3, CARD_2:60; :: thesis: verum