let X be non empty categorial set ; for Y being non empty set
for C1, C2 being strict Categorial Category st the carrier of C1 = X & ( for A, B being Element of X
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C1 iff F in Y ) ) & the carrier of C2 = X & ( for A, B being Element of X
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C2 iff F in Y ) ) holds
C1 = C2
let Y be non empty set ; for C1, C2 being strict Categorial Category st the carrier of C1 = X & ( for A, B being Element of X
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C1 iff F in Y ) ) & the carrier of C2 = X & ( for A, B being Element of X
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C2 iff F in Y ) ) holds
C1 = C2
let C1, C2 be strict Categorial Category; ( the carrier of C1 = X & ( for A, B being Element of X
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C1 iff F in Y ) ) & the carrier of C2 = X & ( for A, B being Element of X
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C2 iff F in Y ) ) implies C1 = C2 )
assume that
A1:
the carrier of C1 = X
and
A2:
for A, B being Element of X
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C1 iff F in Y )
and
A3:
the carrier of C2 = X
and
A4:
for A, B being Element of X
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C2 iff F in Y )
; C1 = C2
the carrier' of C1 = the carrier' of C2
hence
C1 = C2
by A1, A3, Th14; verum