let C, D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( c in dom f implies Im (f,c) = {(f /. c)} )
assume A1: c in dom f ; :: thesis: Im (f,c) = {(f /. c)}
hence Im (f,c) = {(f . c)} by FUNCT_1:59
.= {(f /. c)} by A1, PARTFUN1:def 6 ;
:: thesis: verum