let f be Function; :: thesis: for a, b, c being set st a <> c holds
(f +* (a .--> b)) . c = f . c
let a, b, c be set ; :: thesis: ( a <> c implies (f +* (a .--> b)) . c = f . c )
assume A1: a <> c ; :: thesis: (f +* (a .--> b)) . c = f . c
set g = a .--> b;
dom (a .--> b) = {a} by FUNCOP_1:19;
then not c in dom (a .--> b) by A1, TARSKI:def 1;
hence (f +* (a .--> b)) . c = f . c by Th12; :: thesis: verum