let C, D be non empty set ; :: thesis: for c being Element of C
for d being Element of D
for f being PartFunc of C,D st f = {[c,d]} holds
f /. c = d
let c be Element of C; :: thesis: for d being Element of D
for f being PartFunc of C,D st f = {[c,d]} holds
f /. c = d
let d be Element of D; :: thesis: for f being PartFunc of C,D st f = {[c,d]} holds
f /. c = d
let f be PartFunc of C,D; :: thesis: ( f = {[c,d]} implies f /. c = d )
assume A1: f = {[c,d]} ; :: thesis: f /. c = d
then [c,d] in f by TARSKI:def 1;
then A2: c in dom f by FUNCT_1:1;
f . c = d by A1, GRFUNC_1:6;
hence f /. c = d by A2, PARTFUN1:def 6; :: thesis: verum