for C being composable with_identities preorder CategoryStr st not C is empty holds
ex F being Function of C,(RelOb C) st
( F is bijective & ( for f being morphism of C holds F . f = [(dom f),(cod f)] ) )