let f be Function; :: thesis: for a, b, c being object st a <> c holds
(f +* (a .--> b)) . c = f . c
let a, b, c be object ; :: 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;
not c in dom (a .--> b) by A1, TARSKI:def 1;
hence (f +* (a .--> b)) . c = f . c by Th11; :: thesis: verum