let x be set ; :: thesis: ( x is I -extension implies x is Function-like )
assume x is I -extension ; :: thesis: x is Function-like
then x = I === by DefExtension;
hence x is Function-like ; :: thesis: verum