proposition: Lemma lub_comp2_eq : forall (D1 D2 D3:cpo) (F : D1 -m> D2 -M-> D3), (forall k:D1, continuous (F k)) -> continuous F -> forall (f : natO-m>D1) (g :natO-m>D2), F (lub f) (lub g) == lub ((F@2 f) g).
proof: Proof. intros; apply Ole_antisym; auto. apply (continuous_continuous2 (F:=F)); trivial. Qed.