set f = the onto isometric Function of M,M;
reconsider f = the onto isometric Function of M,M as Function of (TopSpaceMetr M),(TopSpaceMetr M) ;
take f ; :: thesis: ( f is onto & f is isometric )
thus ( f is onto & f is isometric ) ; :: thesis: verum