let R be Relation; :: thesis: ( dom R is finite & rng R is finite implies R is finite )
assume ( dom R is finite & rng R is finite ) ; :: thesis: R is finite
then field R is finite ;
hence R is finite by Th196; :: thesis: verum