now :: thesis: for x being object st x in ISOM V holds
x in Funcs ( the carrier of V, the carrier of V)
let x be object ; :: 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:8; :: thesis: verum
end;
hence ISOM V is Subset of (Funcs ( the carrier of V, the carrier of V)) by TARSKI:def 3; :: thesis: verum