theorem :: BVFUNC14:14

for B, C, D, b, c, d being object
for h being Function st h = (B,C,D) --> (b,c,d) holds
rng h = {(h . B),(h . C),(h . D)} by Lm2;