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