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; :: thesis: verum