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:91
.= A by Th93 ;
:: thesis: verum