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:117
.= {(f /. c)} by A1, PARTFUN1:def 8 ;
:: thesis: verum