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 x is Function of V,V 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