proposition: Lemma SplitRAp :forall (X Y : RSetoid) (f : StepF (Y --> X)) (s : StepF Y) (o : OpenUnit), (SplitR (f <@> s) o) == (SplitR f o <@> SplitR s o).
proof: Proof. intros X Y f s o. apply StepF_Qeq_eq; auto with *. unfold Ap. rewrite <- StepFunction.SplitRMap. apply SplitRAp_Qeq. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunction CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields