let C, D, E be non empty set ; :: thesis: for SE being Subset of E
for c being Element of C
for f being PartFunc of C,D st c in dom f holds
f * (SE --> c) = SE --> (f /. c)
let SE be Subset of E; :: thesis: for c being Element of C
for f being PartFunc of C,D st c in dom f holds
f * (SE --> c) = SE --> (f /. c)
let c be Element of C; :: thesis: for f being PartFunc of C,D st c in dom f holds
f * (SE --> c) = SE --> (f /. c)
let f be PartFunc of C,D; :: thesis: ( c in dom f implies f * (SE --> c) = SE --> (f /. c) )
assume A1: c in dom f ; :: thesis: f * (SE --> c) = SE --> (f /. c)
then f * (SE --> c) = SE --> (f . c) by FUNCOP_1:17;
hence f * (SE --> c) = SE --> (f /. c) by A1, PARTFUN1:def 6; :: thesis: verum