let T be TopSpace; :: thesis: OPD-Meet T = (D-Meet T) || (Open_Domains_of T)
reconsider F = OPD-Meet T as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) ;
reconsider G = (D-Meet T) || (Open_Domains_of T) as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) by FUNCT_2:38;
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-Meet T) . A,B by Th37
.= ((D-Meet T) || (Open_Domains_of T)) . [A,B] by FUNCT_1:72
.= G . A,B ; :: thesis: verum

end;

hence OPD-Meet T = (D-Meet T) || (Open_Domains_of T) by BINOP_1:2; :: thesis: verum