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