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 & c in 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 & c in 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 & c in X holds

(f | X) /. c = f /. c

let f be PartFunc of C,D; :: thesis: ( c in dom f & c in X implies (f | X) /. c = f /. c )

assume ( c in dom f & c in X ) ; :: thesis: (f | X) /. c = f /. c

then c in (dom f) /\ X by XBOOLE_0:def 4;

hence (f | X) /. c = f /. c by Th16; :: thesis: verum

for c being Element of C

for f being PartFunc of C,D st c in dom f & c in 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 & c in 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 & c in X holds

(f | X) /. c = f /. c

let f be PartFunc of C,D; :: thesis: ( c in dom f & c in X implies (f | X) /. c = f /. c )

assume ( c in dom f & c in X ) ; :: thesis: (f | X) /. c = f /. c

then c in (dom f) /\ X by XBOOLE_0:def 4;

hence (f | X) /. c = f /. c by Th16; :: thesis: verum