let X be set ; :: thesis: for C, D being non empty set

for d being Element of D

for f being PartFunc of C,D st d in f .: X holds

ex c being Element of C st

( c in dom f & c in X & d = f . c )

let C, D be non empty set ; :: thesis: for d being Element of D

for f being PartFunc of C,D st d in f .: X holds

ex c being Element of C st

( c in dom f & c in X & d = f . c )

let d be Element of D; :: thesis: for f being PartFunc of C,D st d in f .: X holds

ex c being Element of C st

( c in dom f & c in X & d = f . c )

let f be PartFunc of C,D; :: thesis: ( d in f .: X implies ex c being Element of C st

( c in dom f & c in X & d = f . c ) )

assume d in f .: X ; :: thesis: ex c being Element of C st

( c in dom f & c in X & d = f . c )

then consider x being object such that

A1: x in dom f and

A2: ( x in X & d = f . x ) by FUNCT_1:def 6;

reconsider x = x as Element of C by A1;

take x ; :: thesis: ( x in dom f & x in X & d = f . x )

thus ( x in dom f & x in X & d = f . x ) by A1, A2; :: thesis: verum

for d being Element of D

for f being PartFunc of C,D st d in f .: X holds

ex c being Element of C st

( c in dom f & c in X & d = f . c )

let C, D be non empty set ; :: thesis: for d being Element of D

for f being PartFunc of C,D st d in f .: X holds

ex c being Element of C st

( c in dom f & c in X & d = f . c )

let d be Element of D; :: thesis: for f being PartFunc of C,D st d in f .: X holds

ex c being Element of C st

( c in dom f & c in X & d = f . c )

let f be PartFunc of C,D; :: thesis: ( d in f .: X implies ex c being Element of C st

( c in dom f & c in X & d = f . c ) )

assume d in f .: X ; :: thesis: ex c being Element of C st

( c in dom f & c in X & d = f . c )

then consider x being object such that

A1: x in dom f and

A2: ( x in X & d = f . x ) by FUNCT_1:def 6;

reconsider x = x as Element of C by A1;

take x ; :: thesis: ( x in dom f & x in X & d = f . x )

thus ( x in dom f & x in X & d = f . x ) by A1, A2; :: thesis: verum