thus pr2 h1 is FinSequence of B ; :: thesis: verum