proposition: Lemma isum_p9 f E r: worder r -> sub E (substrate r) -> [/\ fgraph f, domain f = substrate r & allf f ordinalp] -> (forall i, inc i (substrate r -s E) -> Vg f i = \0o) -> ipartial_sum f r (substrate r) = ipartial_sum f r E.
proof: Proof. move => wor esr fp fz. have rr := (@sub_refl (substrate r)). move: (isum_q2 wor fp rr)(isum_q2 wor fp esr) => wo1 wo2. rewrite 2! isum_p0; f_equal; apply:(order_exten (proj1 wo1) (proj1 wo2)). have eq1: (disjointU (restr f (substrate r))) = (disjointU (restr f E)). set_extens t => /isum_q6 [pa pb pc]; apply/isum_q6; split => //. case: (inc_or_not (Q t) E) => // nqe. have: inc (Q t) (substrate r -s E) by apply /setC_P. by move/fz => pz; move: pb; rewrite pz => /in_set0. by apply: esr. move => x y; split. move/(isum_q7 wor fp rr) =>[sa sb sc]. by apply/(isum_q7 wor fp esr); rewrite - eq1. move/(isum_q7 wor fp esr) =>[sa sb sc]. by apply/(isum_q7 wor fp rr); rewrite eq1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)