let x be object ; :: thesis: for f being Function st x in dom f holds
f .: {x} = {(f . x)}
let f be Function; :: thesis: ( x in dom f implies f .: {x} = {(f . x)} )
assume A1: x in dom f ; :: thesis: f .: {x} = {(f . x)}
thus f .: {x} = Im (f,x) by RELAT_1:def 16
.= {(f . x)} by A1, FUNCT_1:59 ; :: thesis: verum