let X be set ; :: thesis:
let D, C 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 set such that
A2: ( x in dom f & x in X & d = f . x ) by A1, FUNCT_1:def 12;
reconsider x = x as Element of C by A2;
take x ; :: thesis:
thus ( x in dom f & x in X ) by A2; :: thesis:
thus d = f /. x by A2, PARTFUN1:def 8; :: thesis:

end;

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

end;

assume that
A4: 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
A5: SD <> f .: X ; :: thesis:
consider x being set such that
A6: ( ( x in SD & not x in f .: X ) or ( x in f .: X & not x in SD ) ) by A5, TARSKI:2;

per cases by A6;

suppose A7: ( x in SD & not x in f .: X ) ; :: thesis:

then reconsider x = x as Element of D ;
consider c being Element of C such that
A8: ( c in dom f & c in X & x = f /. c ) by A4, A7;
x = f . c by A8, PARTFUN1:def 8;
hence contradiction by A7, A8, FUNCT_1:def 12; :: thesis:

end;

suppose A9: ( x in f .: X & not x in SD ) ; :: thesis:

then consider y being set such that
A10: ( y in dom f & y in X & x = f . y ) by FUNCT_1:def 12;
reconsider y = y as Element of C by A10;
x = f /. y by A10, PARTFUN1:def 8;
hence contradiction by A4, A9, A10; :: thesis:

end;

hence contradiction ; :: thesis: