:: deftheorem defines . FUNCTOR0:def 5 :
for C1, C2 being non empty AltGraph
for F being BimapStr over C1,C2
for o being Object of C1 holds F . o = ( the ObjectMap of F . (o,o)) `1 ;