theorem Th63:
for
A,
B,
C,
D,
E,
F,
J,
M being
set for
h being
Function for
A9,
B9,
C9,
D9,
E9,
F9,
J9,
M9 being
set st
h = (((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E,F,J,M}