let A, B, C, D, E, F, J, M, N be set ; :: thesis: for h being Function
for A9, B9, C9, D9, E9, F9, J9, M9, N9 being set st A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 & h . M = M9 & h . N = N9 )
let h be Function; :: thesis: for A9, B9, C9, D9, E9, F9, J9, M9, N9 being set st A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 & h . M = M9 & h . N = N9 )
let A9, B9, C9, D9, E9, F9, J9, M9, N9 be set ; :: thesis: ( A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) implies ( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 & h . M = M9 & h . N = N9 ) )
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: A <> M and
A8: A <> N and
A9: ( B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N ) and
A10: M <> N and
A11: h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) ; :: thesis: ( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 & h . M = M9 & h . N = N9 )
A in dom (A .--> A9) by TARSKI:def 1;
then A13: h . A = (A .--> A9) . A by A11, FUNCT_4:13;
not E in dom (A .--> A9) by A4, TARSKI:def 1;
then A14: h . E = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) . E by A11, FUNCT_4:11
.= E9 by A9, Th62 ;
not N in dom (A .--> A9) by A8, TARSKI:def 1;
then A15: h . N = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) . N by A11, FUNCT_4:11
.= N9 by FUNCT_7:94 ;
not D in dom (A .--> A9) by A3, TARSKI:def 1;
then A16: h . D = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) . D by A11, FUNCT_4:11
.= D9 by A9, Th62 ;
not C in dom (A .--> A9) by A2, TARSKI:def 1;
then A17: h . C = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) . C by A11, FUNCT_4:11;
not J in dom (A .--> A9) by A6, TARSKI:def 1;
then A18: h . J = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) . J by A11, FUNCT_4:11
.= J9 by A9, Th62 ;
not F in dom (A .--> A9) by A5, TARSKI:def 1;
then A19: h . F = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) . F by A11, FUNCT_4:11
.= F9 by A9, Th62 ;
not M in dom (A .--> A9) by A7, TARSKI:def 1;
then A20: h . M = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) . M by A11, FUNCT_4:11
.= M9 by A10, Lm1 ;
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)) +* (M .--> M9)) +* (N .--> N9)) . B by A11, FUNCT_4:11
.= B9 by A9, Th62 ;
hence ( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 & h . M = M9 & h . N = N9 ) by A9, A13, A17, A16, A14, A19, A18, A20, A15, Th62, FUNCOP_1:72; :: thesis: verum