the carrier of R \/ the carrier of S is finite ;
hence sum_of R,S is finite by NECKLA_2:def 3; :: thesis: verum