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 8 :: 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 8 :: thesis: verum