theorem Th35: :: YELLOW20:35

for A, B being non empty reflexive AltGraph
for F being feasible Contravariant FunctorStr over A,B st F is faithful holds
for a, b being Object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g