let B, C, D, b, c, d be set ; :: thesis: ( B <> C & D <> B implies (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = b )
assume that
A1: B <> C and
A2: D <> B ; :: thesis: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = b
set h = ((B .--> b) +* (C .--> c)) +* (D .--> d);
dom (D .--> d) = {D} by FUNCOP_1:13;
then not B in dom (D .--> d) by A2, TARSKI:def 1;
then A3: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = ((B .--> b) +* (C .--> c)) . B by FUNCT_4:11;
dom (C .--> c) = {C} by FUNCOP_1:13;
then not B in dom (C .--> c) by A1, TARSKI:def 1;
hence (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = (B .--> b) . B by A3, FUNCT_4:11
.= b by FUNCOP_1:72 ;
:: thesis: verum