{I : Type u} →
  [inst : DecidableEq I] →
    (R : Type v) →
      [inst_1 : CommSemiring R] →
        (A : I → Type w) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] →
              {B : Type w'} →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra R B] → ({i : I} → A i →ₐ[R] B) ≃ (LinearAlgebra.FreeProduct R A →ₐ[R] B)