let C be Category; :: thesis: for D being non empty non void CatStr st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) holds
( D is Category-like & D is transitive & D is associative & D is reflexive & D is with_identities )
let D be non empty non void CatStr ; :: thesis: ( CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) implies ( D is Category-like & D is transitive & D is associative & D is reflexive & D is with_identities ) )
assume A1: CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) ; :: thesis: ( D is Category-like & D is transitive & D is associative & D is reflexive & D is with_identities )
thus A2: for f, g being Morphism of D holds
( [g,f] in dom the Comp of D iff dom g = cod f ) :: according to CAT_1:def 6 :: thesis: ( D is transitive & D is associative & D is reflexive & D is with_identities )
proof
let f, g be Morphism of D; :: thesis: ( [g,f] in dom the Comp of D iff dom g = cod f )
reconsider ff = f, gg = g as Morphism of C by A1;
A3: ( [gg,ff] in dom the Comp of D iff dom gg = cod ff ) by A1, CAT_1:def 6;
thus ( [g,f] in dom the Comp of D implies dom g = cod f ) :: thesis: ( dom g = cod f implies [g,f] in dom the Comp of D )
proof
assume A4: [g,f] in dom the Comp of D ; :: thesis: dom g = cod f
thus dom g = dom gg by A1
.= cod ff by A4, A1, CAT_1:def 6
.= cod f by A1 ; :: thesis: verum
end;
thus ( dom g = cod f implies [g,f] in dom the Comp of D ) by A1, A3; :: thesis: verum
end;
thus A5: for f, g being Morphism of D st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) :: according to CAT_1:def 7 :: thesis: ( D is associative & D is reflexive & D is with_identities )
proof
let f, g be Morphism of D; :: thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
reconsider ff = f, gg = g as Morphism of C by A1;
assume A6: dom g = cod f ; :: thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
A7: dom gg = cod ff by A1, A6;
then [gg,ff] in dom the Comp of C by CAT_1:def 6;
then A8: the Comp of C . (gg,ff) = gg (*) ff by CAT_1:def 1;
( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A7, CAT_1:def 7;
hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A1, A8, A6, A2, CAT_1:def 1; :: thesis: verum
end;
A9: for f, g being Morphism of D st cod g = dom f holds
for ff, gg being Morphism of C st ff = f & gg = g holds
f (*) g = ff (*) gg
proof
let f, g be Morphism of D; :: thesis: ( cod g = dom f implies for ff, gg being Morphism of C st ff = f & gg = g holds
f (*) g = ff (*) gg )
assume A10: cod g = dom f ; :: thesis: for ff, gg being Morphism of C st ff = f & gg = g holds
f (*) g = ff (*) gg
let ff, gg be Morphism of C; :: thesis: ( ff = f & gg = g implies f (*) g = ff (*) gg )
assume A11: ( ff = f & gg = g ) ; :: thesis: f (*) g = ff (*) gg
A12: cod gg = dom ff by A10, A11, A1;
thus f (*) g = the Comp of D . (f,g) by A10, A2, CAT_1:def 1
.= the Comp of C . (ff,gg) by A1, A11
.= ff (*) gg by A12, CAT_1:16 ; :: thesis: verum
end;
thus for f, g, h being Morphism of D st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f :: according to CAT_1:def 8 :: thesis: ( D is reflexive & D is with_identities )
proof
let f, g, h be Morphism of D; :: thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
reconsider ff = f, gg = g, hh = h as Morphism of C by A1;
assume that
A13: dom h = cod g and
A14: dom g = cod f ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f
A15: ( dom hh = cod gg & dom gg = cod ff ) by A13, A14, A1;
A16: g (*) f = gg (*) ff by A14, A9;
A17: h (*) g = hh (*) gg by A13, A9;
A18: dom (h (*) g) = dom g by A13, A5;
cod (g (*) f) = cod g by A14, A5;
hence h (*) (g (*) f) = hh (*) (gg (*) ff) by A9, A16, A13
.= (hh (*) gg) (*) ff by A15, CAT_1:def 8
.= (h (*) g) (*) f by A14, A9, A17, A18 ;
:: thesis: verum
end;
thus D is reflexive :: thesis: D is with_identities
proof
let b be Element of D; :: according to CAT_1:def 9 :: thesis: not Hom (b,b) = {}
reconsider bb = b as Element of C by A1;
reconsider ii = id bb as Morphism of D by A1;
A19: cod ii = cod (id bb) by A1
.= b ;
dom ii = dom (id bb) by A1
.= b ;
then id bb in Hom (b,b) by A19;
hence Hom (b,b) <> {} ; :: thesis: verum
end;
let a be Element of D; :: according to CAT_1:def 10 :: thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of D holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider aa = a as Element of C by A1;
reconsider ii = id aa as Morphism of D by A1;
A20: cod ii = cod (id aa) by A1
.= a ;
dom ii = dom (id aa) by A1
.= a ;
then reconsider ii = ii as Morphism of a,a by A20, CAT_1:4;
take ii ; :: thesis: for b1 being Element of the carrier of D holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be Element of D; :: thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
reconsider bb = b as Element of C by A1;
thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) :: thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
assume A21: Hom (a,b) <> {} ; :: thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; :: thesis: g (*) ii = g
reconsider gg = g as Morphism of C by A1;
A22: cod gg = cod g by A1
.= bb by A21, CAT_1:5 ;
A23: cod (id aa) = aa ;
A24: dom gg = dom g by A1
.= aa by A21, CAT_1:5 ;
then gg in Hom (aa,bb) by A22;
then reconsider gg = gg as Morphism of aa,bb by CAT_1:def 5;
A25: dom g = dom gg by A1
.= a by A24 ;
cod ii = cod (id aa) by A1
.= a ;
hence g (*) ii = the Comp of D . (g,ii) by A25, A2, CAT_1:def 1
.= the Comp of C . (gg,(id aa)) by A1
.= gg (*) (id aa) by A23, A24, CAT_1:16
.= g by A24, CAT_1:22 ;
:: thesis: verum
end;
assume A26: Hom (b,a) <> {} ; :: thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1
let g be Morphism of b,a; :: thesis: ii (*) g = g
reconsider gg = g as Morphism of C by A1;
A27: dom gg = dom g by A1
.= bb by A26, CAT_1:5 ;
A28: dom (id aa) = aa ;
A29: cod gg = cod g by A1
.= aa by A26, CAT_1:5 ;
then gg in Hom (bb,aa) by A27;
then reconsider gg = gg as Morphism of bb,aa by CAT_1:def 5;
A30: cod g = cod gg by A1
.= a by A29 ;
dom ii = dom (id aa) by A1
.= a ;
hence ii (*) g = the Comp of D . (ii,g) by A30, A2, CAT_1:def 1
.= the Comp of C . ((id aa),gg) by A1
.= (id aa) (*) gg by A28, A29, CAT_1:16
.= g by A29, CAT_1:21 ;
:: thesis: verum