∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} {V3 : Type u_7} {P3 : Type u_8} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : AddTorsor V1 P1] [inst_3 : AddCommGroup V3] [inst_4 : AddTorsor V3 P3]
  [inst_5 : Module k V1] [inst_6 : Module k V3] {ι : Type u_9} {φv : ι → Type u_10} {φp : ι → Type u_11}
  [inst_7 : (i : ι) → AddCommGroup (φv i)] [inst_8 : (i : ι) → Module k (φv i)]
  [inst_9 : (i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (g : P3 →ᵃ[k] P1),
  (AffineMap.pi fp).comp g = AffineMap.pi fun i => (fp i).comp g