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

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