let x, y be set ; :: thesis: for f being Function holds Im (f +* (x .--> y)),x = {y}
let f be Function; :: thesis: Im (f +* (x .--> y)),x = {y}

now

let u be set ; :: thesis: ( ( u in (f +* (x .--> y)) .: {x} implies u = y ) & ( u = y implies u in (f +* (x .--> y)) .: {x} ) )
thus ( u in (f +* (x .--> y)) .: {x} implies u = y ) :: thesis: ( u = y implies u in (f +* (x .--> y)) .: {x} )

proof

assume u in (f +* (x .--> y)) .: {x} ; :: thesis: u = y
then consider z being set such that
A1: ( z in dom (f +* (x .--> y)) & z in {x} & u = (f +* (x .--> y)) . z ) by FUNCT_1:def 12;
z in dom (x .--> y) by A1, FUNCOP_1:19;
then u = (x .--> y) . z by A1, FUNCT_4:14;
hence u = y by A1, FUNCOP_1:13; :: thesis: verum

end;

A2: x in {x} by TARSKI:def 1;
then ( x in dom (x .--> y) & (x .--> y) . x = y ) by FUNCOP_1:13, FUNCOP_1:19;
then ( x in dom (f +* (x .--> y)) & y = (f +* (x .--> y)) . x ) by FUNCT_4:13, FUNCT_4:14;
hence ( u = y implies u in (f +* (x .--> y)) .: {x} ) by A2, FUNCT_1:def 12; :: thesis: verum

end;

hence Im (f +* (x .--> y)),x = {y} by TARSKI:def 1; :: thesis: verum