let C be non empty non void CatStr ; ( not C is void & C is trivial' implies ( C is associative & C is with_identities ) )
assume A1:
( not C is void & C is trivial' )
; ( 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; CAT_1:def 8 C is with_identities
let a be Element of C; CAT_1:def 10 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; 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; ( ( 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; ( 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; verum