let f be Function; :: thesis: for x, y, z being object st f . z <> x holds
(f +~ (x,y)) . z = f . z
let x, y, z be object ; :: thesis: ( f . z <> x implies (f +~ (x,y)) . z = f . z )
assume f . z <> x ; :: thesis: (f +~ (x,y)) . z = f . z
then not f . z in dom (x .--> y) by FUNCOP_1:75;
then not z in dom ((x .--> y) * f) by FUNCT_1:11;
hence (f +~ (x,y)) . z = f . z by Th11; :: thesis: verum