no goals
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
wf : Factors P f
wg : Factors P g
⊢ (factorThru P f wf + factorThru P g wg) ≫ MonoOver.arrow (representative.obj P) = f + g
simp