reconsider C = {[a,R]} as non empty finite a -based array ;
C is arr_computation of R by Th75;
hence ex b₁ being arr_computation of R st
( b₁ is a -based & b₁ is finite ) ; :: thesis: verum