theorem Th1: :: ALTCAT_4:1

for C being category
for o1, o2, o3 being Object of C
for v being Morphism of o1,o2
for u being Morphism of o1,o3
for f being Morphism of o2,o3 st u = f * v & (f ") * f = idm o2 & <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} holds
v = (f ") * u