theorem Th17: :: BVFUNC14:17

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y
for h being Function
for A9, B9, C9, D9 being object st G = {A,B,C,D} & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D)}