let f be Function; :: thesis: for y being object st f just_once_values y holds
Im (f,(f <- y)) = {y}
let y be object ; :: thesis: ( f just_once_values y implies Im (f,(f <- y)) = {y} )
assume A1: f just_once_values y ; :: thesis: Im (f,(f <- y)) = {y}
then f <- y in dom f by Def3;
hence Im (f,(f <- y)) = {(f . (f <- y))} by FUNCT_1:59
.= {y} by A1, Def3 ;
:: thesis: verum