let C be non empty non void CatStr ; :: thesis: ( not C is void & C is trivial' implies ( C is associative & C is with_identities ) )
assume A1: ( not C is void & C is trivial' ) ; :: thesis: ( C is associative & C is with_identities )
thus for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f by A1, ZFMISC_1:def 10; :: according to CAT_1:def 8 :: thesis: C is with_identities
let a be Element of C; :: according to CAT_1:def 10 :: thesis: ex i being Morphism of a,a st
for b being Element of C holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
take i = the Morphism of a,a; :: thesis: for b being Element of C holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
let b be Element of C; :: thesis: ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) by A1, ZFMISC_1:def 10; :: thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) by A1, ZFMISC_1:def 10; :: thesis: verum