let C be non empty non void CatStr ; :: thesis: ( ( for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f ) ) & ( for f, g being Morphism of C st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g ) ) & ( for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f ) & ( for b being Object of C holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of C st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of C st dom g = b holds
g * (id b) = g ) ) ) implies C is Category-like )
set CP = the Comp of C;
set CD = the Source of C;
set CC = the Target of C;
set CI = the Id of C;
assume that
A1:
for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f )
and
A2:
for f, g being Morphism of C st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )
and
A3:
for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
and
A4:
for b being Object of C holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of C st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of C st dom g = b holds
g * (id b) = g ) )
; :: thesis: C is Category-like
thus A5:
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 )
:: according to CAT_1:def 8 :: thesis: ( ( 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 ) ) & ( 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 ) & ( for b being Element of the carrier 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 ) ) ) )
thus A6:
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 )
:: thesis: ( ( 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 ) & ( for b being Element of the carrier 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 ) ) ) )proof
let f,
g be
Element of the
carrier' of
C;
:: thesis: ( the Source of C . g = the Target of C . f implies ( 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 ) )
assume A7:
the
Source of
C . g = the
Target of
C . f
;
:: thesis: ( 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 )
( the
Source of
C . g = dom g & the
Target of
C . f = cod f )
;
then
(
dom (g * f) = dom f &
cod (g * f) = cod g &
[g,f] in dom the
Comp of
C & the
Source of
C . (g * f) = dom (g * f) & the
Target of
C . (g * f) = cod (g * f) )
by A2, A5, A7;
hence
( 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 )
by Def4;
:: thesis: verum
end;
thus
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
:: thesis: for b being Element of the carrier 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 ) )proof
let f,
g,
h be
Element of the
carrier' of
C;
:: thesis: ( the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f implies the Comp of C . h,(the Comp of C . g,f) = the Comp of C . (the Comp of C . h,g),f )
assume A8:
( the
Source of
C . h = the
Target of
C . g & the
Source of
C . g = the
Target of
C . f )
;
:: thesis: the Comp of C . h,(the Comp of C . g,f) = the Comp of C . (the Comp of C . h,g),f
A9:
( the
Source of
C . h = dom h & the
Target of
C . g = cod g & the
Source of
C . g = dom g & the
Target of
C . f = cod f )
;
(
[g,f] in dom the
Comp of
C &
[h,g] in dom the
Comp of
C )
by A5, A8;
then A10:
(
g * f = the
Comp of
C . g,
f &
h * g = the
Comp of
C . h,
g )
by Def4;
( the
Source of
C . (the Comp of C . h,g) = the
Source of
C . g & the
Target of
C . (the Comp of C . g,f) = the
Target of
C . g )
by A6, A8;
then
(
[h,(g * f)] in dom the
Comp of
C &
[(h * g),f] in dom the
Comp of
C )
by A5, A8, A10;
then
( the
Comp of
C . h,
(g * f) = h * (g * f) & the
Comp of
C . (h * g),
f = (h * g) * f )
by Def4;
hence
the
Comp of
C . h,
(the Comp of C . g,f) = the
Comp of
C . (the Comp of C . h,g),
f
by A3, A8, A9, A10;
:: thesis: verum
end;
let b be Element of the carrier of C; :: thesis: ( 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 ) )
( dom (id b) = b & cod (id b) = b & id b = the Id of C . b )
by A4;
hence
( the Source of C . (the Id of C . b) = b & the Target of C . (the Id of C . b) = b )
; :: thesis: ( ( 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 ) )
thus
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
:: thesis: 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
let g be Element of the carrier' of C; :: thesis: ( the Source of C . g = b implies the Comp of C . g,(the Id of C . b) = g )
assume A12:
the Source of C . g = b
; :: thesis: the Comp of C . g,(the Id of C . b) = g
( cod (id b) = b & id b = the Id of C . b )
by A4;
then
( the Target of C . (the Id of C . b) = b & the Source of C . g = dom g )
;
then
( g * (id b) = g & [g,(the Id of C . b)] in dom the Comp of C )
by A4, A5, A12;
hence
the Comp of C . g,(the Id of C . b) = g
by Def4; :: thesis: verum