let A, B, C, D, E be set ; :: thesis: for h being Function
for A', B', C', D', E' being set st h = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') holds
dom h = {A,B,C,D,E}
let h be Function; :: thesis: for A', B', C', D', E' being set st h = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') holds
dom h = {A,B,C,D,E}
let A', B', C', D', E' be set ; :: thesis: ( h = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') implies dom h = {A,B,C,D,E} )
assume A1: h = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') ; :: thesis: dom h = {A,B,C,D,E}
dom ((B .--> B') +* (C .--> C')) = (dom (B .--> B')) \/ (dom (C .--> C')) by FUNCT_4:def 1;
then dom (((B .--> B') +* (C .--> C')) +* (D .--> D')) = ((dom (B .--> B')) \/ (dom (C .--> C'))) \/ (dom (D .--> D')) by FUNCT_4:def 1;
then dom ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) = (((dom (B .--> B')) \/ (dom (C .--> C'))) \/ (dom (D .--> D'))) \/ (dom (E .--> E')) by FUNCT_4:def 1;
then A2: dom (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A')) = ((((dom (B .--> B')) \/ (dom (C .--> C'))) \/ (dom (D .--> D'))) \/ (dom (E .--> E'))) \/ (dom (A .--> A')) by FUNCT_4:def 1;
A3: dom (B .--> B') = {B} by FUNCOP_1:19;
A4: dom (C .--> C') = {C} by FUNCOP_1:19;
A5: dom (D .--> D') = {D} by FUNCOP_1:19;
dom (E .--> E') = {E} by FUNCOP_1:19;
then dom (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A')) = {A} \/ ((({B} \/ {C}) \/ {D}) \/ {E}) by A2, A3, A4, A5, FUNCOP_1:19
.= {A} \/ (({B,C} \/ {D}) \/ {E}) by ENUMSET1:41
.= {A} \/ ({B,C,D} \/ {E}) by ENUMSET1:43
.= {A} \/ {B,C,D,E} by ENUMSET1:46
.= {A,B,C,D,E} by ENUMSET1:47 ;
hence dom h = {A,B,C,D,E} by A1; :: thesis: verum