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

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