let A, B, C, D, E be set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: ( 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 ;
not C in dom (A .--> A9) by ;
then A14: h . C = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) . C by ;
not B in dom (D .--> D9) by ;
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 ;
then A17: h . E = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) . E by ;
E in dom (E .--> E9) by TARSKI:def 1;
then A19: h . E = (E .--> E9) . E by ;
not C in dom (D .--> D9) by ;
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 ;
then A21: h . C = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . C by ;
C in dom (C .--> C9) by TARSKI:def 1;
then A23: h . C = (C .--> C9) . C by ;
not D in dom (A .--> A9) by ;
then A24: h . D = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) . D by ;
not D in dom (E .--> E9) by ;
then A25: h . D = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . D by ;
D in dom (D .--> D9) by TARSKI:def 1;
then A26: h . D = (D .--> D9) . D by ;
not B in dom (A .--> A9) by ;
then A27: h . B = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) . B by ;
not B in dom (E .--> E9) by ;
then A28: h . B = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . B by ;
not B in dom (C .--> C9) by ;
then h . B = (B .--> B9) . B by ;
hence ( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 ) by ; :: thesis: verum