let A, B, C, D, E, F, J be set ; :: thesis: for h being Function
for A', B', C', D', E', F', J' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' )
let h be Function; :: thesis: for A', B', C', D', E', F', J' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' )
let A', B', C', D', E', F', J' be set ; :: thesis: ( 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') implies ( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' ) )
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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') ; :: thesis: ( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' )
A9: dom (A .--> A') = {A} by FUNCOP_1:19;
then A in dom (A .--> A') by TARSKI:def 1;
then A10: h . A = (A .--> A') . A by A8, FUNCT_4:14;
not J in dom (A .--> A') by A6, A9, TARSKI:def 1;
then A11: h . J = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) . J by A8, FUNCT_4:12
.= J' by A7, Th40 ;
not F in dom (A .--> A') by A5, A9, TARSKI:def 1;
then A12: h . F = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) . F by A8, FUNCT_4:12
.= F' by A7, Th40 ;
not E in dom (A .--> A') by A4, A9, TARSKI:def 1;
then A13: h . E = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) . E by A8, FUNCT_4:12
.= E' by A7, Th40 ;
not D in dom (A .--> A') by A3, A9, TARSKI:def 1;
then A14: h . D = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) . D by A8, FUNCT_4:12
.= D' by A7, Th40 ;
not C in dom (A .--> A') by A2, A9, TARSKI:def 1;
then A15: h . C = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) . C by A8, FUNCT_4:12
.= C' by A7, Th40 ;
not B in dom (A .--> A') by A1, A9, TARSKI:def 1;
then h . B = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) . B by A8, FUNCT_4:12
.= B' by A7, Th40 ;
hence ( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' ) by A10, A15, A14, A13, A12, A11, FUNCOP_1:87; :: thesis: verum