let A, B, C, D, E, F, J, M be set ; :: thesis: for h being Function
for A', B', C', D', E', F', J', M' being set st h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J,M}
let h be Function; :: thesis: for A', B', C', D', E', F', J', M' being set st h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J,M}
let A', B', C', D', E', F', J', M' be set ; :: thesis: ( h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') implies dom h = {A,B,C,D,E,F,J,M} )
assume A1: h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') ; :: thesis: dom h = {A,B,C,D,E,F,J,M}
A2: dom (A .--> A') = {A} by FUNCOP_1:19;
dom (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) = {M,B,C,D,E,F,J} by Th53
.= {M} \/ {B,C,D,E,F,J} by ENUMSET1:56
.= {B,C,D,E,F,J,M} by ENUMSET1:61 ;
then dom ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A')) = {B,C,D,E,F,J,M} \/ {A} by A2, FUNCT_4:def 1
.= {A,B,C,D,E,F,J,M} by ENUMSET1:62 ;
hence dom h = {A,B,C,D,E,F,J,M} by A1; :: thesis: verum