theorem Th76: :: BVFUNC14:76

for A, B, C, D, E, F, J, M, N being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9, M9, N9 being set st A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 & h . M = M9 & h . N = N9 )