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