let A, B, C, D, E be set ; for h being Function
for A', B', C', D', E' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' )
let h be Function; for A', B', C', D', E' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' )
let A', B', C', D', E' be set ; ( A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & h = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') implies ( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' ) )
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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A')
; ( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' )
A12:
dom (A .--> A') = {A}
by FUNCOP_1:19;
then
A in dom (A .--> A')
by TARSKI:def 1;
then A13:
h . A = (A .--> A') . A
by A11, FUNCT_4:14;
not C in dom (A .--> A')
by A2, A12, TARSKI:def 1;
then A14:
h . C = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) . C
by A11, FUNCT_4:12;
A15:
dom (D .--> D') = {D}
by FUNCOP_1:19;
then
not B in dom (D .--> D')
by A6, TARSKI:def 1;
then A16:
(((B .--> B') +* (C .--> C')) +* (D .--> D')) . B = ((B .--> B') +* (C .--> C')) . B
by FUNCT_4:12;
not E in dom (A .--> A')
by A4, A12, TARSKI:def 1;
then A17:
h . E = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) . E
by A11, FUNCT_4:12;
A18:
dom (E .--> E') = {E}
by FUNCOP_1:19;
then
E in dom (E .--> E')
by TARSKI:def 1;
then A19:
h . E = (E .--> E') . E
by A17, FUNCT_4:14;
not C in dom (D .--> D')
by A8, A15, TARSKI:def 1;
then A20:
(((B .--> B') +* (C .--> C')) +* (D .--> D')) . C = ((B .--> B') +* (C .--> C')) . C
by FUNCT_4:12;
not C in dom (E .--> E')
by A9, A18, TARSKI:def 1;
then A21:
h . C = (((B .--> B') +* (C .--> C')) +* (D .--> D')) . C
by A14, FUNCT_4:12;
A22:
dom (C .--> C') = {C}
by FUNCOP_1:19;
then
C in dom (C .--> C')
by TARSKI:def 1;
then A23:
h . C = (C .--> C') . C
by A21, A20, FUNCT_4:14;
not D in dom (A .--> A')
by A3, A12, TARSKI:def 1;
then A24:
h . D = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) . D
by A11, FUNCT_4:12;
not D in dom (E .--> E')
by A10, A18, TARSKI:def 1;
then A25:
h . D = (((B .--> B') +* (C .--> C')) +* (D .--> D')) . D
by A24, FUNCT_4:12;
D in dom (D .--> D')
by A15, TARSKI:def 1;
then A26:
h . D = (D .--> D') . D
by A25, FUNCT_4:14;
not B in dom (A .--> A')
by A1, A12, TARSKI:def 1;
then A27:
h . B = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) . B
by A11, FUNCT_4:12;
not B in dom (E .--> E')
by A7, A18, TARSKI:def 1;
then A28:
h . B = (((B .--> B') +* (C .--> C')) +* (D .--> D')) . B
by A27, FUNCT_4:12;
not B in dom (C .--> C')
by A5, A22, TARSKI:def 1;
then
h . B = (B .--> B') . B
by A28, A16, FUNCT_4:12;
hence
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' )
by A13, A23, A26, A19, FUNCOP_1:87; verum