let f be Function; :: thesis: for a, A, b, B, c, C being set st a <> b & a <> c holds
(((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = A
let a, A, b, B, c, C be set ; :: thesis: ( a <> b & a <> c implies (((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = A )
assume ( a <> b & a <> c ) ; :: thesis: (((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = A
hence (((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = (f +* (a .--> A)) . a by FUNCT_4:97
.= A by Th96 ;
:: thesis: verum