let C, D be non empty set ; :: thesis: for f being PartFunc of C,D ex g being Function of C,D st
for c being Element of C st c in dom f holds
g . c = f /. c
let f be PartFunc of C,D; :: thesis: ex g being Function of C,D st
for c being Element of C st c in dom f holds
g . c = f /. c
consider g being Function of C,D such that
A1: for x being object st x in dom f holds
g . x = f . x by FUNCT_2:71;
take g ; :: thesis: for c being Element of C st c in dom f holds
g . c = f /. c
let c be Element of C; :: thesis: ( c in dom f implies g . c = f /. c )
assume A2: c in dom f ; :: thesis: g . c = f /. c
then g . c = f . c by A1;
hence g . c = f /. c by A2, PARTFUN1:def 6; :: thesis: verum