∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1]
  [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : AddCommGroup V3]
  [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) (p : P1), f (g p) = (f.comp g) p