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