theorem :: BVFUNC14:11

for B, C, D, b, c, d being object holds dom ((B,C,D) --> (b,c,d)) = {B,C,D} by FUNCT_4:128;