theorem Th7: :: ALTCAT_3:7

for C being category
for o1, o2, o3 being Object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso holds
( B * A is iso & (B * A) " = (A ") * (B ") )