let f be Function; :: thesis: for a, b, n, m, x being set st x <> m & x <> a holds
((f +* (a .--> b)) +* (m .--> n)) . x = f . x
let a, b, n, m, x be set ; :: thesis: ( x <> m & x <> a implies ((f +* (a .--> b)) +* (m .--> n)) . x = f . x )
assume that
A1: x <> m and
A2: x <> a ; :: thesis: ((f +* (a .--> b)) +* (m .--> n)) . x = f . x
set mn = m .--> n;
set nm = a .--> b;
dom (a .--> b) = {a} by FUNCOP_1:13;
then A3: not x in dom (a .--> b) by A2, TARSKI:def 1;
dom (m .--> n) = {m} by FUNCOP_1:13;
then not x in dom (m .--> n) by A1, TARSKI:def 1;
hence ((f +* (a .--> b)) +* (m .--> n)) . x = (f +* (a .--> b)) . x by Th12
.= f . x by A3, Th12 ;
:: thesis: verum