let f be Function; :: thesis: for C, D, c, d being object st C <> D holds
((f +* (C .--> c)) +* (D .--> d)) . C = c
let C, D, c, d be object ; :: thesis: ( C <> D implies ((f +* (C .--> c)) +* (D .--> d)) . C = c )
set h = (f +* (C .--> c)) +* (D .--> d);
assume C <> D ; :: thesis: ((f +* (C .--> c)) +* (D .--> d)) . C = c
then not C in dom (D .--> d) by TARSKI:def 1;
then A2: ((f +* (C .--> c)) +* (D .--> d)) . C = (f +* (C .--> c)) . C by FUNCT_4:11;
C in dom (C .--> c) by TARSKI:def 1;
hence ((f +* (C .--> c)) +* (D .--> d)) . C = (C .--> c) . C by A2, FUNCT_4:13
.= c by FUNCOP_1:72 ;
:: thesis: verum