let f be Function; :: thesis: for C, D, c, d being set st C <> D holds
((f +* (C .--> c)) +* (D .--> d)) . C = c
let C, D, c, d be set ; :: thesis: ( C <> D implies ((f +* (C .--> c)) +* (D .--> d)) . C = c )
assume A1: C <> D ; :: thesis: ((f +* (C .--> c)) +* (D .--> d)) . C = c
set h = (f +* (C .--> c)) +* (D .--> d);
A2: dom (C .--> c) = {C} by FUNCOP_1:19;
dom (D .--> d) = {D} by FUNCOP_1:19;
then not C in dom (D .--> d) by A1, TARSKI:def 1;
then A3: ((f +* (C .--> c)) +* (D .--> d)) . C = (f +* (C .--> c)) . C by FUNCT_4:12;
C in dom (C .--> c) by A2, TARSKI:def 1;
hence ((f +* (C .--> c)) +* (D .--> d)) . C = (C .--> c) . C by A3, FUNCT_4:14
.= c by FUNCOP_1:87 ;
:: thesis: verum