(M : Type u_3) →
  (N : Type u_4) →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        (M' : Type u_6) →
          (N' : Type u_7) →
            [inst_2 : AddZeroClass N'] → [inst_3 : AddZeroClass M'] → (M × N) × M' × N' ≃+ (M × M') × N × N'