∀ {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] (maps : {i : I} → A i →ₐ[R] B) (f : LinearAlgebra.FreeProduct R A →ₐ[R] B),
  (∀ (i : I), f.comp (LinearAlgebra.FreeProduct.ι R A i) = maps) →
    f = (LinearAlgebra.FreeProduct.lift R A) fun {i} => maps