theorem Th64:
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
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}