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