theorem Th26: :: BVFUNC14:26

for A, B, C, D, E being set
for h being Function
for A9, B9, C9, D9, E9 being set st A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 )