A1: rng f = [#] V by FUNCT_2:def 3;
hence rng (f " ) = the carrier of V by TOPS_2:62; :: according to FUNCT_2:def 3 :: thesis: f " is isometric
let x, y be Element of V; :: according to VECTMETR:def 3 :: thesis: dist x,y = dist ((f " ) . x),((f " ) . y)
A2: rng f = the carrier of V by A1;
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