let T be TopSpace; :: thesis: OPD-Union T = (D-Union T) || (Open_Domains_of T)
A1: Open_Domains_of T c= Domains_of T by Th35;
then reconsider F = OPD-Union T as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) by FUNCT_2:7;
[:(Open_Domains_of T),(Open_Domains_of T):] c= [:(Domains_of T),(Domains_of T):] by A1, ZFMISC_1:96;
then reconsider G = (D-Union T) || (Open_Domains_of T) as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) by FUNCT_2:32;
for A, B being Element of Open_Domains_of T holds F . (A,B) = G . (A,B)
proof
let A, B be Element of Open_Domains_of T; :: thesis: F . (A,B) = G . (A,B)
thus F . (A,B) = (D-Union T) . (A,B) by Th36
.= ((D-Union T) || (Open_Domains_of T)) . [A,B] by FUNCT_1:49
.= G . (A,B) ; :: thesis: verum
end;
hence OPD-Union T = (D-Union T) || (Open_Domains_of T) by BINOP_1:2; :: thesis: verum