now :: thesis: for x being object st x in ISOM V holds

x in Funcs ( the carrier of V, the carrier of V)

hence
ISOM V is Subset of (Funcs ( the carrier of V, the carrier of V))
by TARSKI:def 3; :: thesis: verumx 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;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