take omega --> omega ; :: thesis: omega --> omega is infinite
dom (omega --> omega) = omega ;
hence omega --> omega is infinite ; :: thesis: verum