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