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