let C be composable with_identities CategoryStr ; :: thesis: for f1, f2 being morphism of C st f1 |> f2 holds
( dom (f1 (*) f2) = dom f2 & cod (f1 (*) f2) = cod f1 )
let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 implies ( dom (f1 (*) f2) = dom f2 & cod (f1 (*) f2) = cod f1 ) )
assume A1: f1 |> f2 ; :: thesis: ( dom (f1 (*) f2) = dom f2 & cod (f1 (*) f2) = cod f1 )

per cases ( C is empty or not C is empty ) ;

suppose A2: C is empty ; :: thesis: ( dom (f1 (*) f2) = dom f2 & cod (f1 (*) f2) = cod f1 )

thus dom (f1 (*) f2) = the Object of C by A2, CAT_6:def 18
.= dom f2 by A2, CAT_6:def 18 ; :: thesis: cod (f1 (*) f2) = cod f1
thus cod (f1 (*) f2) = the Object of C by A2, CAT_6:def 19
.= cod f1 by A2, CAT_6:def 19 ; :: thesis: verum

end;

suppose A3: not C is empty ; :: thesis: ( dom (f1 (*) f2) = dom f2 & cod (f1 (*) f2) = cod f1 )

[f1,f2] in dom the composition of C by A1, CAT_6:def 2;
then [f1,f2] in dom (CompMap C) by CAT_6:def 29;
then A4: (SourceMap C) . f1 = (TargetMap C) . f2 by A3, CAT_6:36;
A5: f1 (*) f2 = the composition of C . (f1,f2) by A1, CAT_6:def 3
.= (CompMap C) . (f1,f2) by CAT_6:def 29 ;
thus dom (f1 (*) f2) = (SourceMap C) . (f1 (*) f2) by A3, CAT_6:def 30
.= (SourceMap C) . f2 by A4, A5, CAT_6:37
.= dom f2 by A3, CAT_6:def 30 ; :: thesis: cod (f1 (*) f2) = cod f1
thus cod (f1 (*) f2) = (TargetMap C) . (f1 (*) f2) by A3, CAT_6:def 31
.= (TargetMap C) . f1 by A4, A5, CAT_6:37
.= cod f1 by A3, CAT_6:def 31 ; :: thesis: verum

end;

end;