let C, D be non empty set ; :: thesis: for SD being Subset of D
for c being Element of C
for f being PartFunc of C,D holds
( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )
let SD be Subset of D; :: thesis: for c being Element of C
for f being PartFunc of C,D holds
( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )
let c be Element of C; :: thesis: for f being PartFunc of C,D holds
( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )
let f be PartFunc of C,D; :: thesis: ( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )
thus ( c in f " SD implies ( [c,(f /. c)] in f & f /. c in SD ) ) :: thesis: ( [c,(f /. c)] in f & f /. c in SD implies c in f " SD )

proof

assume c in f " SD ; :: thesis: ( [c,(f /. c)] in f & f /. c in SD )
then A1: ( [c,(f . c)] in f & f . c in SD ) by GRFUNC_1:87;
then c in dom f by FUNCT_1:8;
hence ( [c,(f /. c)] in f & f /. c in SD ) by A1, PARTFUN1:def 8; :: thesis: verum

end;

assume A2: ( [c,(f /. c)] in f & f /. c in SD ) ; :: thesis: c in f " SD
then c in dom f by Th65;
hence c in f " SD by A2, Th44; :: thesis: verum