let R be Relation; :: thesis: ( dom R is finite & rng R is finite implies R is finite )
assume that
A1: dom R is finite and
A2: rng R is finite ; :: thesis: R is finite
field R is finite by A1, A2;
hence R is finite by Th86; :: thesis: verum