is mentioned by

Thm* g:(ABC). (Id,Id) o g = g	[comp2_id_l]
Thm* h:(A'A1A2), g1:(A1B), g2:(A2C), f1:(BB'), f2:(CC'). (f1,f2) o (g1,g2) o h = (f1 o g1,f2 o g2) o h	[comp2_comp2_assoc]
Thm* h:(A'A), g:(ABC), f1:(BB'), f2:(CC'). (f1,f2) o g o h = (f1,f2) o g o h	[comp2_comp_assoc]

Try larger context: Graphs