let X be set ; :: thesis: for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in (dom f) /\ X holds
(f | X) /. c = f /. c
let C, D be non empty set ; :: thesis: for c being Element of C
for f being PartFunc of C,D st c in (dom f) /\ X holds
(f | X) /. c = f /. c
let c be Element of C; :: thesis: for f being PartFunc of C,D st c in (dom f) /\ X holds
(f | X) /. c = f /. c
let f be PartFunc of C,D; :: thesis: ( c in (dom f) /\ X implies (f | X) /. c = f /. c )
assume c in (dom f) /\ X ; :: thesis: (f | X) /. c = f /. c
then c in dom (f | X) by RELAT_1:61;
hence (f | X) /. c = f /. c by Th15; :: thesis: verum