let A, B, x be set ; :: thesis: ( x in B implies A --> x is Function of A,B )
assume A1: x in B ; :: thesis: A --> x is Function of A,B
then A2: {x} c= B by ZFMISC_1:37;
( dom (A --> x) = A & rng (A --> x) c= {x} ) by Th19;
then ( dom (A --> x) = A & rng (A --> x) c= B ) by A2, XBOOLE_1:1;
hence A --> x is Function of A,B by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum