let A, B, C, D, E be set ; :: thesis: for h being Function
for A9, B9, C9, D9, E9 being set st h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E}
let h be Function; :: thesis: for A9, B9, C9, D9, E9 being set st h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E}
let A9, B9, C9, D9, E9 be set ; :: thesis: ( h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) implies dom h = {A,B,C,D,E} )
assume A1: h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) ; :: thesis: dom h = {A,B,C,D,E}
A2: ( dom (D .--> D9) = {D} & dom (E .--> E9) = {E} ) by FUNCOP_1:13;
dom ((B .--> B9) +* (C .--> C9)) = (dom (B .--> B9)) \/ (dom (C .--> C9)) by FUNCT_4:def 1;
then dom (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) = ((dom (B .--> B9)) \/ (dom (C .--> C9))) \/ (dom (D .--> D9)) by FUNCT_4:def 1;
then dom ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) = (((dom (B .--> B9)) \/ (dom (C .--> C9))) \/ (dom (D .--> D9))) \/ (dom (E .--> E9)) by FUNCT_4:def 1;
then A3: dom (((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9)) = ((((dom (B .--> B9)) \/ (dom (C .--> C9))) \/ (dom (D .--> D9))) \/ (dom (E .--> E9))) \/ (dom (A .--> A9)) by FUNCT_4:def 1;
( dom (B .--> B9) = {B} & dom (C .--> C9) = {C} ) by FUNCOP_1:13;
then dom (((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9)) = {A} \/ ((({B} \/ {C}) \/ {D}) \/ {E}) by A3, A2, FUNCOP_1:13
.= {A} \/ (({B,C} \/ {D}) \/ {E}) by ENUMSET1:1
.= {A} \/ ({B,C,D} \/ {E}) by ENUMSET1:3
.= {A} \/ {B,C,D,E} by ENUMSET1:6
.= {A,B,C,D,E} by ENUMSET1:7 ;
hence dom h = {A,B,C,D,E} by A1; :: thesis: verum