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