proposition: Lemma saturation_of_union r f g: equivalence r -> function f -> function g -> (forall i, inc i (source f) -> sub (Vf f i) (substrate r)) -> source f = source g -> (forall i, inc i (source f) -> saturation_of r (Vf f i) = Vf g i) -> saturation_of r (union_image (\Po(substrate r)) f) = union_image (\Po(substrate r)) g.
proof: Proof. move=> er ff fg als sfsg alsat. have fc: function (canon_proj r) by fprops. have U1sr: sub (union_image (\Po (substrate r)) f) (substrate r). by move => t /setU_P [z zt /Zo_P [/setP_P h _]]; apply: h. set_extens x. move/(idvalue_cprojP er U1sr) => [zu [z /setU_P [v zv]] /Zo_P [] /setP_P vsr [i isf fi] sc]. move:(als _ isf) => pa. apply/setU_P; exists (Vf g i); rewrite -(alsat _ isf). apply/(idvalue_cprojP er pa); split => //; exists z => //; ue. apply: Zo_i; first by apply/setP_P=> t /(idvalue_cprojP er pa) [ ok _]. rewrite - sfsg; ex_tac. move => /setU_P [z xz /Zo_P [/setP_P zr [i isr zv]]]. move: xz; rewrite - sfsg in isr; rewrite zv - (alsat _ isr). move/(idvalue_cprojP er (als _ isr)) => [pa [t pb pc]]. apply/(idvalue_cprojP er U1sr); split => //; exists t => //. apply /setU_P; exists (Vf f i) => //; apply:Zo_i; last by ex_tac. by apply /setP_P; apply: als. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)