let C, D be CatStr ; :: thesis: ( CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C, the Id of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D, the Id of D #) & C is Category-like implies D is Category-like )
assume A1: CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C, the Id of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D, the Id of D #) ; :: thesis: ( not C is Category-like or D is Category-like )
assume that
A2: for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) and
A3: for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . ( the Comp of C . (g,f)) = the Source of C . f & the Target of C . ( the Comp of C . (g,f)) = the Target of C . g ) and
A4: for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . (h,( the Comp of C . (g,f))) = the Comp of C . (( the Comp of C . (h,g)),f) and
A5: for b being Element of C holds
( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C st the Source of C . g = b holds
the Comp of C . (g,( the Id of C . b)) = g ) ) ; :: according to CAT_1:def 5 :: thesis: D is Category-like
thus ( ( for f, g being Element of the carrier' of D holds
( [g,f] in dom the Comp of D iff the Source of D . g = the Target of D . f ) ) & ( for f, g being Element of the carrier' of D st the Source of D . g = the Target of D . f holds
( the Source of D . ( the Comp of D . (g,f)) = the Source of D . f & the Target of D . ( the Comp of D . (g,f)) = the Target of D . g ) ) & ( for f, g, h being Element of the carrier' of D st the Source of D . h = the Target of D . g & the Source of D . g = the Target of D . f holds
the Comp of D . (h,( the Comp of D . (g,f))) = the Comp of D . (( the Comp of D . (h,g)),f) ) & ( for b being Element of D holds
( the Source of D . ( the Id of D . b) = b & the Target of D . ( the Id of D . b) = b & ( for f being Element of the carrier' of D st the Target of D . f = b holds
the Comp of D . (( the Id of D . b),f) = f ) & ( for g being Element of the carrier' of D st the Source of D . g = b holds
the Comp of D . (g,( the Id of D . b)) = g ) ) ) ) by A1, A2, A3, A4, A5; :: according to CAT_1:def 5 :: thesis: verum