let C be non empty composable with_identities CategoryStr ; :: thesis: for f1, f2 being morphism of C holds
( f1 |> f2 iff dom f1 = cod f2 )
let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 iff dom f1 = cod f2 )
A1: dom f1 = (SourceMap C) . f1 by CAT_6:def 30;
A2: cod f2 = (TargetMap C) . f2 by CAT_6:def 31;

hereby :: thesis: ( dom f1 = cod f2 implies f1 |> f2 )

assume f1 |> f2 ; :: thesis: dom f1 = cod f2
then [f1,f2] in dom the composition of C by CAT_6:def 2;
then [f1,f2] in dom (CompMap C) by CAT_6:def 29;
hence dom f1 = cod f2 by A1, A2, CAT_6:36; :: thesis: verum

end;

assume dom f1 = cod f2 ; :: thesis: f1 |> f2
then (SourceMap C) . f1 = (TargetMap C) . f2 by A1, CAT_6:def 31;
then [f1,f2] in dom (CompMap C) by CAT_6:36;
then [f1,f2] in dom the composition of C by CAT_6:def 29;
hence f1 |> f2 by CAT_6:def 2; :: thesis: verum