let C be composable with_identities CategoryStr ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) <> {} ) ; :: thesis: ( ( 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 ) :: thesis: ( f2 is identity implies f2 * f1 = f1 )

proof

assume f1 is identity ; :: thesis: f2 * f1 = f2
then A4: f1 is Object of C by A2, CAT_6:22;
thus f2 * f1 = f2 (*) f1 by A1, Def4
.= f2 by A2, A4, A3, CAT_6:23 ; :: thesis: verum

end;

assume f2 is identity ; :: thesis: 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 ; :: thesis: verum