set R = R1 \/ R2;
R1 \/ R2 is finitary

proof

let a be object ; :: according to PROOFS_1:def 1 :: thesis: ( a in dom (R1 \/ R2) implies a is finite set )
assume a in dom (R1 \/ R2) ; :: thesis: a is finite set
then a in (dom R1) \/ (dom R2) by XTUPLE_0:23;
then ( a in dom R1 or a in dom R2 ) by XBOOLE_0:def 3;
hence a is finite set by Def1; :: thesis: verum

end;

hence R1 \/ R2 is Rule ; :: thesis: verum