<*> REAL is real-valued ;
hence ex b₁ being FinSequence st
( b₁ is real-valued & b₁ is complex-valued ) ; :: thesis: verum