let C, D be non empty set ; 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; for f being PartFunc of C,D st dom f = {c} holds
f = {[c,(f /. c)]}
let f be PartFunc of C,D; ( dom f = {c} implies f = {[c,(f /. c)]} )
assume
dom f = {c}
; 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; verum