now

let x be set ; :: thesis: ( x in ISOM V implies x in Funcs the carrier of V,the carrier of V )
assume x in ISOM V ; :: thesis: x in Funcs the carrier of V,the carrier of V
then ex f being Function of V,V st
( f = x & f is isometric ) by Def4;
hence x in Funcs the carrier of V,the carrier of V by FUNCT_2:11; :: thesis: verum

end;

hence ISOM V is Subset of (Funcs the carrier of V,the carrier of V) by TARSKI:def 3; :: thesis: verum