let A, B, C, D, E, F, J be set ; for h being Function
for A9, B9, C9, D9, E9, F9, J9 being set st A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 )
let h be Function; for A9, B9, C9, D9, E9, F9, J9 being set st A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 )
let A9, B9, C9, D9, E9, F9, J9 be set ; ( A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) implies ( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 ) )
assume that
A1:
A <> B
and
A2:
A <> C
and
A3:
A <> D
and
A4:
A <> E
and
A5:
A <> F
and
A6:
A <> J
and
A7:
( B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J )
and
A8:
h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9)
; ( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 )
A in dom (A .--> A9)
by TARSKI:def 1;
then A10:
h . A = (A .--> A9) . A
by A8, FUNCT_4:13;
not J in dom (A .--> A9)
by A6, TARSKI:def 1;
then A11: h . J =
((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) . J
by A8, FUNCT_4:11
.=
J9
by A7, Th37
;
not F in dom (A .--> A9)
by A5, TARSKI:def 1;
then A12: h . F =
((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) . F
by A8, FUNCT_4:11
.=
F9
by A7, Th37
;
not E in dom (A .--> A9)
by A4, TARSKI:def 1;
then A13: h . E =
((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) . E
by A8, FUNCT_4:11
.=
E9
by A7, Th37
;
not D in dom (A .--> A9)
by A3, TARSKI:def 1;
then A14: h . D =
((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) . D
by A8, FUNCT_4:11
.=
D9
by A7, Th37
;
not C in dom (A .--> A9)
by A2, TARSKI:def 1;
then A15: h . C =
((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) . C
by A8, FUNCT_4:11
.=
C9
by A7, Th37
;
not B in dom (A .--> A9)
by A1, TARSKI:def 1;
then h . B =
((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) . B
by A8, FUNCT_4:11
.=
B9
by A7, Th37
;
hence
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 )
by A10, A15, A14, A13, A12, A11, FUNCOP_1:72; verum