theorem Th77:
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
h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E,F,J,M,N}