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 that
A1: i in dom A and
A2: A is Hall ; :: thesis: card (A . i) >= 1
set J = {i};
{i} c= dom A by A1, ZFMISC_1:31;
then A3: card {i} <= card (union (A,{i})) by A2;
assume A4: card (A . i) < 1 ; :: thesis: contradiction
union (A,{i}) = A . i by A1, Th5;
hence contradiction by A4, A3, CARD_2:42; :: thesis: verum