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 consider f being Function of V,V such that
A1: f = x and
f is isometric by Def4;
thus x in Funcs the carrier of V,the carrier of V by A1, 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