let C1, C2 be strict discrete category; :: thesis: ( the carrier of C1 = X & the carrier of C2 = X implies C1 = C2 )
assume A15: ( the carrier of C1 = X & the carrier of C2 = X ) ; :: thesis: C1 = C2
A16: for C being with_identities discrete CategoryStr
for x being object st not C is empty holds
( x in the composition of C iff ex f being morphism of C st x = [[f,f],f] )
proof
let C be with_identities discrete CategoryStr ; :: thesis: for x being object st not C is empty holds
( x in the composition of C iff ex f being morphism of C st x = [[f,f],f] )
let x be object ; :: thesis: ( not C is empty implies ( x in the composition of C iff ex f being morphism of C st x = [[f,f],f] ) )
assume A17: not C is empty ; :: thesis: ( x in the composition of C iff ex f being morphism of C st x = [[f,f],f] )
hereby :: thesis: ( ex f being morphism of C st x = [[f,f],f] implies x in the composition of C )
assume A18: x in the composition of C ; :: thesis: ex f being morphism of C st x = [[f,f],f]
then consider y, f being object such that
A19: ( y in [: the carrier of C, the carrier of C:] & f in the carrier of C & x = [y,f] ) by ZFMISC_1:def 2;
reconsider f = f as morphism of C by A19;
take f = f; :: thesis: x = [[f,f],f]
consider f1, f2 being object such that
A20: ( f1 in the carrier of C & f2 in the carrier of C & y = [f1,f2] ) by A19, ZFMISC_1:def 2;
reconsider f1 = f1, f2 = f2 as morphism of C by A20;
A21: [f1,f2] in dom the composition of C by A20, A19, A18, XTUPLE_0:def 12;
A22: f1 |> f2 by A20, A19, A18, XTUPLE_0:def 12;
then ( f1 = f2 & f1 (*) f2 = f2 ) by Th21;
then the composition of C . (f1,f2) = f2 by A21, Def3, Def2;
then the composition of C . y = f2 by A20, BINOP_1:def 1;
then f = f2 by A18, A19, FUNCT_1:1;
hence x = [[f,f],f] by A22, A20, A19, Th21; :: thesis: verum
end;
given f being morphism of C such that A23: x = [[f,f],f] ; :: thesis: x in the composition of C
consider f1 being morphism of C such that
A24: ( f1 |> f & f1 is left_identity ) by A17, Def6, Def12;
A25: f is identity by Def15;
A26: f1 = f1 (*) f by A25, A24, Def5
.= f by A24 ;
f = f (*) f by A24, A26;
then the composition of C . (f,f) = f by A24, A26, Def3;
then the composition of C . [f,f] = f by BINOP_1:def 1;
hence x in the composition of C by A23, A24, A26, FUNCT_1:1; :: thesis: verum
end;
per cases ( the carrier of C1 is empty or not the carrier of C1 is empty ) ;
suppose the carrier of C1 is empty ; :: thesis: C1 = C2
hence C1 = C2 by A15; :: thesis: verum
end;
suppose not the carrier of C1 is empty ; :: thesis: C1 = C2
then A27: ( not C1 is empty & not C2 is empty ) by A15;
for x being object holds
( x in the composition of C1 iff x in the composition of C2 )
proof
let x be object ; :: thesis: ( x in the composition of C1 iff x in the composition of C2 )
hereby :: thesis: ( x in the composition of C2 implies x in the composition of C1 )
assume x in the composition of C1 ; :: thesis: x in the composition of C2
then consider f being morphism of C1 such that
A28: x = [[f,f],f] by A27, A16;
reconsider f1 = f as morphism of C2 by A15;
x = [[f1,f1],f1] by A28;
hence x in the composition of C2 by A27, A16; :: thesis: verum
end;
assume x in the composition of C2 ; :: thesis: x in the composition of C1
then consider f being morphism of C2 such that
A29: x = [[f,f],f] by A27, A16;
reconsider f1 = f as morphism of C1 by A15;
x = [[f1,f1],f1] by A29;
hence x in the composition of C1 by A27, A16; :: thesis: verum
end;
hence C1 = C2 by A15, TARSKI:2; :: thesis: verum
end;
end;