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 A1: dom f = {c} ; :: thesis: f = {[c,(f /. c)]}
then A2: c in dom f by TARSKI:def 1;
f = {[c,(f . c)]} by A1, GRFUNC_1:18;
hence f = {[c,(f /. c)]} by A2, PARTFUN1:def 8; :: thesis: verum