<*> D = {} ;
hence ex b₁ being FinSequence of D st b₁ is empty ; :: thesis: verum