set R = R1 \/ R2;
A1: ( dom (R1 \/ R2) = (dom R1) \/ (dom R2) & dom R1 c= Fin Fml & dom R2 c= Fin Fml ) by Def2, XTUPLE_0:23;
( rng (R1 \/ R2) = (rng R1) \/ (rng R2) & rng R1 c= Fml & rng R2 c= Fml ) by Def2, RELAT_1:12;
then rng (R1 \/ R2) c= Fml by XBOOLE_1:8;
hence R1 \/ R2 is Rule of Fml by A1, Def2, XBOOLE_1:8; :: thesis: verum