let C be composable with_identities CategoryStr ; for a, b, c being Object of C
for f1 being Morphism of a,b
for f2 being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
( ( f1 is identity implies f2 * f1 = f2 ) & ( f2 is identity implies f2 * f1 = f1 ) )
let a, b, c be Object of C; for f1 being Morphism of a,b
for f2 being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
( ( f1 is identity implies f2 * f1 = f2 ) & ( f2 is identity implies f2 * f1 = f1 ) )
let f1 be Morphism of a,b; for f2 being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
( ( f1 is identity implies f2 * f1 = f2 ) & ( f2 is identity implies f2 * f1 = f1 ) )
let f2 be Morphism of b,c; ( Hom (a,b) <> {} & Hom (b,c) <> {} implies ( ( f1 is identity implies f2 * f1 = f2 ) & ( f2 is identity implies f2 * f1 = f1 ) ) )
assume A1:
( Hom (a,b) <> {} & Hom (b,c) <> {} )
; ( ( f1 is identity implies f2 * f1 = f2 ) & ( f2 is identity implies f2 * f1 = f1 ) )
then A2:
not C is empty
;
A3:
f2 |> f1
by A1, Th17;
thus
( f1 is identity implies f2 * f1 = f2 )
( f2 is identity implies f2 * f1 = f1 )
assume
f2 is identity
; f2 * f1 = f1
then A5:
f2 is Object of C
by A2, CAT_6:22;
thus f2 * f1 =
f2 (*) f1
by A1, Def4
.=
f1
by A2, A5, A3, CAT_6:23
; verum