thus Im r is zero by Def2; :: thesis: