∀ {R : Type u} {M : Type v} {N : Type w} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : SizeOf R] [inst_6 : SizeOf M] [inst_7 : SizeOf N]
  (toFun : M → N) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x)
  (exists_companion' : ∃ B, ∀ (x y : M), toFun (x + y) = toFun x + toFun y + (B x) y),
  sizeOf { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' } =
    1 + sizeOf exists_companion'