let Y be set ; :: thesis: for f being Function st Y in dom (" f) holds
(" f) . Y = f " Y
let f be Function; :: thesis: ( Y in dom (" f) implies (" f) . Y = f " Y )
dom (" f) = bool (rng f) by Def2;
hence ( Y in dom (" f) implies (" f) . Y = f " Y ) by Def2; :: thesis: verum