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