theorem :: CAT_4:2

for o, m being set holds CatStr(# the carrier of (c1Cat (o,m)), the carrier' of (c1Cat (o,m)), the Source of (c1Cat (o,m)), the Target of (c1Cat (o,m)), the Comp of (c1Cat (o,m)) #) = 1Cat (o,m) ;