theorem Th23: :: YELLOW20:23

for A, B being AltCatStr st A,B have_the_same_composition holds
for a1, a2 being Object of A
for b1, b2 being Object of B
for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1,a2^> <> {} & <^b1,b2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of b1,b2 st f = g holds
f in <^o1,o2^>