let A, B, C, D be object ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum