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

proof

assume that
A1: c in dom f and
A2: c in SC ; :: thesis: [c,(f /. c)] in f | SC
[c,(f . c)] in f | SC by A1, A2, GRFUNC_1:22;
hence [c,(f /. c)] in f | SC by A1, PARTFUN1:def 6; :: thesis: verum

end;

assume [c,(f /. c)] in f | SC ; :: thesis: ( c in dom f & c in SC )
then c in dom (f | SC) by FUNCT_1:1;
then c in (dom f) /\ SC by RELAT_1:61;
hence ( c in dom f & c in SC ) by XBOOLE_0:def 4; :: thesis: verum