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

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