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
A1: ( O = {o} & M = {m} & d = m .--> o & c = m .--> o & p = m,m .--> m & i = o .--> m & C = CatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m) #) ) ;
reconsider C = C as non empty non void CatStr by A1;
( ( 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 ) ) & ( 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 ) ) ) ) by A1, Lm1;
hence CatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m) #) is strict Category by A1, Def8; :: thesis: verum