let C, D be non empty set ; for c being Element of C
for f being PartFunc of C,D st c in dom f holds
Im (f,c) = {(f /. c)}
let c be Element of C; for f being PartFunc of C,D st c in dom f holds
Im (f,c) = {(f /. c)}
let f be PartFunc of C,D; ( c in dom f implies Im (f,c) = {(f /. c)} )
assume A1:
c in dom f
; Im (f,c) = {(f /. c)}
hence Im (f,c) =
{(f . c)}
by FUNCT_1:59
.=
{(f /. c)}
by A1, PARTFUN1:def 6
;
verum