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 A1: c in f " SD ; :: thesis: ( [c,(f /. c)] in f & f /. c in SD )
then A2: f . c in SD by GRFUNC_1:26;
A3: [c,(f . c)] in f by A1, GRFUNC_1:26;
then c in dom f by FUNCT_1:1;
hence ( [c,(f /. c)] in f & f /. c in SD ) by A3, A2, PARTFUN1:def 6; :: thesis: verum

end;

assume that
A4: [c,(f /. c)] in f and
A5: f /. c in SD ; :: thesis: c in f " SD
c in dom f by A4, Th46;
hence c in f " SD by A5, Th26; :: thesis: verum