theorem Th15: :: BVFUNC14:15

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