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

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