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

((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