let A, B be set ; :: thesis: for X being non empty set

for x being Element of X st x in B holds

A --> x is Function of A,B

let X be non empty set ; :: thesis: for x being Element of X st x in B holds

A --> x is Function of A,B

let x be Element of X; :: thesis: ( x in B implies A --> x is Function of A,B )

A1: rng (A --> x) c= {x} by Th13;

A2: dom (A --> x) = A ;

assume A3: x in B ; :: thesis: A --> x is Function of A,B

then {x} c= B by ZFMISC_1:31;

then rng (A --> x) c= B by A1;

hence A --> x is Function of A,B by A3, A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

for x being Element of X st x in B holds

A --> x is Function of A,B

let X be non empty set ; :: thesis: for x being Element of X st x in B holds

A --> x is Function of A,B

let x be Element of X; :: thesis: ( x in B implies A --> x is Function of A,B )

A1: rng (A --> x) c= {x} by Th13;

A2: dom (A --> x) = A ;

assume A3: x in B ; :: thesis: A --> x is Function of A,B

then {x} c= B by ZFMISC_1:31;

then rng (A --> x) c= B by A1;

hence A --> x is Function of A,B by A3, A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum