let A, B, C, D be object ; for h being Function
for A9, B9, C9, D9 being object st h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
dom h = {A,B,C,D}
let h be Function; for A9, B9, C9, D9 being object st h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
dom h = {A,B,C,D}
let A9, B9, C9, D9 be object ; ( h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) implies dom h = {A,B,C,D} )
assume A1:
h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9)
; dom h = {A,B,C,D}
dom ((B .--> B9) +* (C .--> C9)) = (dom (B .--> B9)) \/ (dom (C .--> C9))
by FUNCT_4:def 1;
then A2:
dom (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) = ((dom (B .--> B9)) \/ (dom (C .--> C9))) \/ (dom (D .--> D9))
by FUNCT_4:def 1;
dom ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9)) =
(({B} \/ (dom (C .--> C9))) \/ (dom (D .--> D9))) \/ (dom (A .--> A9))
by A2, FUNCT_4:def 1
.=
(({B} \/ {C}) \/ (dom (D .--> D9))) \/ (dom (A .--> A9))
.=
(({B} \/ {C}) \/ {D}) \/ (dom (A .--> A9))
.=
{A} \/ (({B} \/ {C}) \/ {D})
.=
{A} \/ ({B,C} \/ {D})
by ENUMSET1:1
.=
{A} \/ {B,C,D}
by ENUMSET1:3
.=
{A,B,C,D}
by ENUMSET1:4
;
hence
dom h = {A,B,C,D}
by A1; verum