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 dom f & f /. c in SD ) iff [c,(f /. c)] in SD | f )
let SD be Subset of D; :: thesis: for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD | f )
let c be Element of C; :: thesis: for f being PartFunc of C,D holds
( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD | f )
let f be PartFunc of C,D; :: thesis: ( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD | f )
thus ( c in dom f & f /. c in SD implies [c,(f /. c)] in SD | f ) :: thesis: ( [c,(f /. c)] in SD | f implies ( c in dom f & f /. c in SD ) )

proof

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

end;

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