consider O, M being non empty set , d, c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function of O,M, C being CatStr such that
O = {o}
and
M = {m}
and
d = m .--> o
and
c = m .--> o
and
p = m,m .--> m
and
i = o .--> m
and
A1:
C = CatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m) #)
;
reconsider C = C as non empty non void CatStr by A1;
A2:
( ( 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 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 ) ) ) )
by A1, Lm1;
( ( 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 ) ) & ( 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 ) ) )
by A1, Lm1;
hence
CatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m) #) is strict Category
by A1, A2, Def8; verum