for I being set
for C being category
for A being ObjectsFamily of I,C
for C1, C2 being Object of C st C1 is A -CatCoproduct-like & C2 is A -CatCoproduct-like holds
C1,C2 are_iso