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 h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J}
let h be Function; :: thesis: for A', B', C', D', E', F', J' being set st h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J}
let A', B', C', D', E', F', J' be set ; :: thesis: ( h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') implies dom h = {A,B,C,D,E,F,J} )
assume A1: h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') ; :: thesis: dom h = {A,B,C,D,E,F,J}
A2: dom (A .--> A') = {A} by FUNCOP_1:19;
dom h = (dom ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J'))) \/ (dom (A .--> A')) by A1, FUNCT_4:def 1
.= {J,B,C,D,E,F} \/ (dom (A .--> A')) by Th41
.= ({B,C,D,E,F} \/ {J}) \/ {A} by A2, ENUMSET1:51
.= {B,C,D,E,F,J} \/ {A} by ENUMSET1:55
.= {A,B,C,D,E,F,J} by ENUMSET1:56 ;
hence dom h = {A,B,C,D,E,F,J} ; :: thesis: verum