let C, D be non empty set ; :: thesis: for c being Element of C

for f being PartFunc of C,D st dom f = {c} holds

f = {[c,(f /. c)]}

let c be Element of C; :: thesis: for f being PartFunc of C,D st dom f = {c} holds

f = {[c,(f /. c)]}

let f be PartFunc of C,D; :: thesis: ( dom f = {c} implies f = {[c,(f /. c)]} )

assume dom f = {c} ; :: thesis: f = {[c,(f /. c)]}

then ( c in dom f & f = {[c,(f . c)]} ) by GRFUNC_1:7, TARSKI:def 1;

hence f = {[c,(f /. c)]} by PARTFUN1:def 6; :: thesis: verum

for f being PartFunc of C,D st dom f = {c} holds

f = {[c,(f /. c)]}

let c be Element of C; :: thesis: for f being PartFunc of C,D st dom f = {c} holds

f = {[c,(f /. c)]}

let f be PartFunc of C,D; :: thesis: ( dom f = {c} implies f = {[c,(f /. c)]} )

assume dom f = {c} ; :: thesis: f = {[c,(f /. c)]}

then ( c in dom f & f = {[c,(f . c)]} ) by GRFUNC_1:7, TARSKI:def 1;

hence f = {[c,(f /. c)]} by PARTFUN1:def 6; :: thesis: verum