let V be non empty Reflexive discerning MetrStruct ; :: thesis: for f being isometric Function of V,V holds f " is isometric
let f be isometric Function of V,V; :: thesis: f " is isometric
A1: rng f = [#] V by Def3;
rng f = [#] V by Def3;
hence rng (f " ) = the carrier of V by TOPS_2:62; :: according to VECTMETR:def 3 :: thesis: for x, y being Element of V holds dist x,y = dist ((f " ) . x),((f " ) . y)
let x, y be Element of V; :: thesis: dist x,y = dist ((f " ) . x),((f " ) . y)
A2: rng f = the carrier of V by Def3;
then A3: dom (f " ) = [#] V by TOPS_2:62;
A4: y = (id (rng f)) . y by A2, FUNCT_1:35
.= (f * (f " )) . y by A1, TOPS_2:65
.= f . ((f " ) . y) by A3, FUNCT_1:23 ;
x = (id (rng f)) . x by A2, FUNCT_1:35
.= (f * (f " )) . x by A1, TOPS_2:65
.= f . ((f " ) . x) by A3, FUNCT_1:23 ;
hence dist x,y = dist ((f " ) . x),((f " ) . y) by A4, Def3; :: thesis: verum