thus pr1 h1 is FinSequence of A ; :: thesis: