let A, B, C, D, E, F, J be set ; :: thesis: for h being Function
for A9, B9, C9, D9, E9, F9, J9 being set st h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E,F,J}
let h be Function; :: thesis: for A9, B9, C9, D9, E9, F9, J9 being set st h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E,F,J}
let A9, B9, C9, D9, E9, F9, J9 be set ; :: thesis: ( h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) implies dom h = {A,B,C,D,E,F,J} )
A1: dom (A .--> A9) = {A} by FUNCOP_1:13;
assume h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) ; :: thesis: dom h = {A,B,C,D,E,F,J}
then dom h = (dom ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9))) \/ (dom (A .--> A9)) by FUNCT_4:def 1
.= {J,B,C,D,E,F} \/ (dom (A .--> A9)) by Th41
.= ({B,C,D,E,F} \/ {J}) \/ {A} by A1, ENUMSET1:11
.= {B,C,D,E,F,J} \/ {A} by ENUMSET1:15
.= {A,B,C,D,E,F,J} by ENUMSET1:16 ;
hence dom h = {A,B,C,D,E,F,J} ; :: thesis: verum