let C be category; :: thesis: for a, b, c, d being Object of C
for f1 being Morphism of a,b
for f2 being Morphism of b,c
for f3 being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
f3 * (f2 * f1) = (f3 * f2) * f1
let a, b, c, d be Object of C; :: thesis: for f1 being Morphism of a,b
for f2 being Morphism of b,c
for f3 being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
f3 * (f2 * f1) = (f3 * f2) * f1
let f1 be Morphism of a,b; :: thesis: for f2 being Morphism of b,c
for f3 being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
f3 * (f2 * f1) = (f3 * f2) * f1
let f2 be Morphism of b,c; :: thesis: for f3 being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
f3 * (f2 * f1) = (f3 * f2) * f1
let f3 be Morphism of c,d; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} implies f3 * (f2 * f1) = (f3 * f2) * f1 )
assume A1: Hom (a,b) <> {} ; :: thesis: ( not Hom (b,c) <> {} or not Hom (c,d) <> {} or f3 * (f2 * f1) = (f3 * f2) * f1 )
assume A2: Hom (b,c) <> {} ; :: thesis: ( not Hom (c,d) <> {} or f3 * (f2 * f1) = (f3 * f2) * f1 )
assume A3: Hom (c,d) <> {} ; :: thesis: f3 * (f2 * f1) = (f3 * f2) * f1
A4: Hom (a,c) <> {} by A1, A2, Th22;
A5: Hom (b,d) <> {} by A2, A3, Th22;
A6: ( f3 |> f2 & f2 |> f1 ) by A1, A2, A3, Th17;
f3 * f2 |> f1 by A5, A1, Th17;
then A7: f3 (*) f2 |> f1 by A2, A3, Def4;
f3 |> f2 * f1 by A4, A3, Th17;
then A8: f3 |> f2 (*) f1 by A1, A2, Def4;
thus f3 * (f2 * f1) = f3 (*) (f2 * f1) by A3, A4, Def4
.= f3 (*) (f2 (*) f1) by A1, A2, Def4
.= (f3 (*) f2) (*) f1 by A6, A7, A8, CAT_6:def 10
.= (f3 * f2) (*) f1 by A2, A3, Def4
.= (f3 * f2) * f1 by A1, A5, Def4 ; :: thesis: verum