let F be Function; :: thesis: for x, y, z being set st x <> z holds
(F +* (x .--> y)) . z = F . z
let x, y, z be set ; :: thesis: ( x <> z implies (F +* (x .--> y)) . z = F . z )
assume x <> z ; :: thesis: (F +* (x .--> y)) . z = F . z
then not z in dom (x .--> y) by TARSKI:def 1;
hence (F +* (x .--> y)) . z = F . z by FUNCT_4:11; :: thesis: verum