let X be non empty categorial set ; :: thesis:
let Y be non empty set ; :: thesis:
let C1, C2 be strict Categorial Category; :: thesis:
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 ) ; :: thesis:
the carrier' of C1 = the carrier' of C2

let x be object ; :: thesis:
assume x in the carrier' of C1 ; :: thesis:
then reconsider m = x as Morphism of C1 ;
reconsider a = dom m, b = cod m as Category by Th12;
consider f being Functor of a,b such that
A5: m = [[a,b],f] by Def6;
f in Y by A1, A2, A5;
then x is Morphism of C2 by A1, A4, A5;
hence x in the carrier' of C2 ; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier' of C2 ; :: thesis:
then reconsider m = x as Morphism of C2 ;
reconsider a = dom m, b = cod m as Category by Th12;
consider f being Functor of a,b such that
A6: m = [[a,b],f] by Def6;
f in Y by A3, A4, A6;
then x is Morphism of C1 by A2, A3, A6;
hence x in the carrier' of C1 ; :: thesis:

end;