let A, B, C, D, E, F, J, M, N be set ; :: thesis: for h being Function
for A', B', C', D', E', F', J', M', N' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' & h . M = M' & h . N = N' )
let h be Function; :: thesis: for A', B', C', D', E', F', J', M', N' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' & h . M = M' & h . N = N' )
let A', B', C', D', E', F', J', M', N' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') implies ( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' & h . M = M' & h . N = N' ) )
assume A1: ( 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') ) ; :: thesis: ( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' & h . M = M' & h . N = N' )
A2: dom (A .--> A') = {A} by FUNCOP_1:19;
A3: h . A = A'

proof

A in dom (A .--> A') by A2, TARSKI:def 1;
then h . A = (A .--> A') . A by A1, FUNCT_4:14;
hence h . A = A' by FUNCOP_1:87; :: thesis: verum

end;

A4: h . B = B'

proof

not B in dom (A .--> A') by A1, A2, TARSKI:def 1;
then h . B = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) . B by A1, FUNCT_4:12
.= B' by A1, Th21 ;
hence h . B = B' ; :: thesis: verum

end;

A5: h . C = C'

proof

not C in dom (A .--> A') by A1, A2, TARSKI:def 1;
then h . C = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) . C by A1, FUNCT_4:12;
hence h . C = C' by A1, Th21; :: thesis: verum

end;

A6: h . D = D'

proof

not D in dom (A .--> A') by A1, A2, TARSKI:def 1;
then h . D = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) . D by A1, FUNCT_4:12
.= D' by A1, Th21 ;
hence h . D = D' ; :: thesis: verum

end;

A7: h . E = E'

proof

not E in dom (A .--> A') by A1, A2, TARSKI:def 1;
then h . E = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) . E by A1, FUNCT_4:12
.= E' by A1, Th21 ;
hence h . E = E' ; :: thesis: verum

end;

A8: h . F = F'

proof

not F in dom (A .--> A') by A1, A2, TARSKI:def 1;
then h . F = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) . F by A1, FUNCT_4:12
.= F' by A1, Th21 ;
hence h . F = F' ; :: thesis: verum

end;

A9: h . J = J'

proof

not J in dom (A .--> A') by A1, A2, TARSKI:def 1;
then h . J = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) . J by A1, FUNCT_4:12
.= J' by A1, Th21 ;
hence h . J = J' ; :: thesis: verum

end;

A10: h . M = M'

proof

not M in dom (A .--> A') by A1, A2, TARSKI:def 1;
then h . M = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) . M by A1, FUNCT_4:12
.= M' by A1, TH15 ;
hence h . M = M' ; :: thesis: verum

end;

h . N = N'

proof

not N in dom (A .--> A') by A1, A2, TARSKI:def 1;
then h . N = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) . N by A1, FUNCT_4:12
.= N' by FUNCT_7:96 ;
hence h . N = N' ; :: thesis: verum

end;

hence ( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' & h . M = M' & h . N = N' ) by A3, A4, A5, A6, A7, A8, A9, A10; :: thesis: verum