theorem Th2: :: ALTCAT_4:2

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