proposition: Lemma eqoaddo (W' : normedModType K) F (f g : T -> V) (h : T -> W') : [o_F f + [o_F f of g] of h] =o_F f.
proof: Proof. by apply: equivoLR. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule