theorem Th2: :: YELLOW18:2

for A, B being category
for F, G being contravariant Functor of A,B st ( for a being Object of A holds F . a = G . a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . f ) holds
FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)