for B, C, D, b, c, d being object st B <> C & D <> B holds
((B,C,D) --> (b,c,d)) . B = b by FUNCT_4:134;