let C, D be non empty set ; :: thesis: for d being Element of D
for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds
f /. c = d ) holds
f = (dom f) --> d
let d be Element of D; :: thesis: for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds
f /. c = d ) holds
f = (dom f) --> d
let f be PartFunc of C,D; :: thesis: ( ( for c being Element of C st c in dom f holds
f /. c = d ) implies f = (dom f) --> d )
assume A1: for c being Element of C st c in dom f holds
f /. c = d ; :: thesis: f = (dom f) --> d

now :: thesis: for x being object st x in dom f holds
f . x = d

let x be object ; :: thesis: ( x in dom f implies f . x = d )
assume A2: x in dom f ; :: thesis: f . x = d
then reconsider x1 = x as Element of C ;
f /. x1 = d by A1, A2;
hence f . x = d by A2, PARTFUN1:def 6; :: thesis: verum

end;

hence f = (dom f) --> d by FUNCOP_1:11; :: thesis: verum