theorem Th16: :: BVFUNC14:16

for A, B, C, D being object
for h being Function
for A9, B9, C9, D9 being object st h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
dom h = {A,B,C,D}