let T be TopSpace; :: thesis: CLD-Union T = (D-Union T) || (Closed_Domains_of T)
A1: Closed_Domains_of T c= Domains_of T by Th31;
then reconsider F = CLD-Union T as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) by FUNCT_2:7;
[:(Closed_Domains_of T),(Closed_Domains_of T):] c= [:(Domains_of T),(Domains_of T):] by A1, ZFMISC_1:96;
then reconsider G = (D-Union T) || (Closed_Domains_of T) as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) by FUNCT_2:32;
for A, B being Element of Closed_Domains_of T holds F . (A,B) = G . (A,B)

proof

let A, B be Element of Closed_Domains_of T; :: thesis: F . (A,B) = G . (A,B)
thus F . (A,B) = (D-Union T) . (A,B) by Th32
.= ((D-Union T) || (Closed_Domains_of T)) . [A,B] by FUNCT_1:49
.= G . (A,B) ; :: thesis: verum

end;

hence CLD-Union T = (D-Union T) || (Closed_Domains_of T) by BINOP_1:2; :: thesis: verum