let A, B, C, D, E be set ; for h being Function
for A9, B9, C9, D9, E9 being set st A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 )
let h be Function; for A9, B9, C9, D9, E9 being set st A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 )
let A9, B9, C9, D9, E9 be set ; ( A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) implies ( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 ) )
assume that
A1:
A <> B
and
A2:
A <> C
and
A3:
A <> D
and
A4:
A <> E
and
A5:
B <> C
and
A6:
B <> D
and
A7:
B <> E
and
A8:
C <> D
and
A9:
C <> E
and
A10:
D <> E
and
A11:
h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9)
; ( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 )
A in dom (A .--> A9)
by TARSKI:def 1;
then A13:
h . A = (A .--> A9) . A
by A11, FUNCT_4:13;
not C in dom (A .--> A9)
by A2, TARSKI:def 1;
then A14:
h . C = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) . C
by A11, FUNCT_4:11;
not B in dom (D .--> D9)
by A6, TARSKI:def 1;
then A16:
(((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . B = ((B .--> B9) +* (C .--> C9)) . B
by FUNCT_4:11;
not E in dom (A .--> A9)
by A4, TARSKI:def 1;
then A17:
h . E = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) . E
by A11, FUNCT_4:11;
E in dom (E .--> E9)
by TARSKI:def 1;
then A19:
h . E = (E .--> E9) . E
by A17, FUNCT_4:13;
not C in dom (D .--> D9)
by A8, TARSKI:def 1;
then A20:
(((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . C = ((B .--> B9) +* (C .--> C9)) . C
by FUNCT_4:11;
not C in dom (E .--> E9)
by A9, TARSKI:def 1;
then A21:
h . C = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . C
by A14, FUNCT_4:11;
C in dom (C .--> C9)
by TARSKI:def 1;
then A23:
h . C = (C .--> C9) . C
by A21, A20, FUNCT_4:13;
not D in dom (A .--> A9)
by A3, TARSKI:def 1;
then A24:
h . D = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) . D
by A11, FUNCT_4:11;
not D in dom (E .--> E9)
by A10, TARSKI:def 1;
then A25:
h . D = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . D
by A24, FUNCT_4:11;
D in dom (D .--> D9)
by TARSKI:def 1;
then A26:
h . D = (D .--> D9) . D
by A25, FUNCT_4:13;
not B in dom (A .--> A9)
by A1, TARSKI:def 1;
then A27:
h . B = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) . B
by A11, FUNCT_4:11;
not B in dom (E .--> E9)
by A7, TARSKI:def 1;
then A28:
h . B = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . B
by A27, FUNCT_4:11;
not B in dom (C .--> C9)
by A5, TARSKI:def 1;
then
h . B = (B .--> B9) . B
by A28, A16, FUNCT_4:11;
hence
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 )
by A13, A23, A26, A19, FUNCOP_1:72; verum