let C, D be non empty set ; :: thesis: for SC being Subset of C
for c being Element of C
for d being Element of D st c in SC holds
(SC --> d) /. c = d
let SC be Subset of C; :: thesis: for c being Element of C
for d being Element of D st c in SC holds
(SC --> d) /. c = d
let c be Element of C; :: thesis: for d being Element of D st c in SC holds
(SC --> d) /. c = d
let d be Element of D; :: thesis: ( c in SC implies (SC --> d) /. c = d )
assume A1: c in SC ; :: thesis: (SC --> d) /. c = d
then ( dom (SC --> d) = SC & (SC --> d) . c = d ) by FUNCOP_1:7, FUNCOP_1:13;
hence (SC --> d) /. c = d by A1, PARTFUN1:def 6; :: thesis: verum