consider c being Cardinal such that
A1: dom R = c by Def1;
thus dom R is cardinal by A1; :: thesis: verum