let X be set ; :: thesis:
let C, D be non empty set ; :: thesis:
let SD be Subset of D; :: thesis:
let f be PartFunc of C,D; :: thesis:
thus ( SD = f .: X implies for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) ) :: thesis:

assume A1: SD = f .: X ; :: thesis:
let d be Element of D; :: thesis:
thus ( d in SD implies ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) :: thesis:

assume d in SD ; :: thesis:
then consider x being object such that
A2: x in dom f and
A3: x in X and
A4: d = f . x by A1, FUNCT_1:def 6;
reconsider x = x as Element of C by A2;
take x ; :: thesis:
thus ( x in dom f & x in X ) by A2, A3; :: thesis:
thus d = f /. x by A2, A4, PARTFUN1:def 6; :: thesis:

end;

given c being Element of C such that A5: c in dom f and
A6: ( c in X & d = f /. c ) ; :: thesis:
f /. c = f . c by A5, PARTFUN1:def 6;
hence d in SD by A1, A5, A6, FUNCT_1:def 6; :: thesis:

end;

assume that
A7: for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) and
A8: SD <> f .: X ; :: thesis:
consider x being object such that
A9: ( ( x in SD & not x in f .: X ) or ( x in f .: X & not x in SD ) ) by A8, TARSKI:2;

then reconsider x = x as Element of D ;
consider c being Element of C such that
A11: c in dom f and
A12: c in X and
A13: x = f /. c by A7, A10;
x = f . c by A11, A13, PARTFUN1:def 6;
hence contradiction by A10, A11, A12, FUNCT_1:def 6; :: thesis:

end;

then consider y being object such that
A15: y in dom f and
A16: y in X and
A17: x = f . y by FUNCT_1:def 6;
reconsider y = y as Element of C by A15;
x = f /. y by A15, A17, PARTFUN1:def 6;
hence contradiction by A7, A14, A15, A16; :: thesis:

end;