for x, y being Real holds R2Homeomorphism . [x,y] = <*x,y*> by Def2;
hence R2Homeomorphism is being_homeomorphism by TOPREAL6:76; :: thesis: verum