consider f being isometric Function of M,M;
reconsider f = f as Function of (TopSpaceMetr M),(TopSpaceMetr M) ;
take f ; :: thesis: f is isometric
thus f is isometric by Def2; :: thesis: verum