let C be composable with_identities CategoryStr ; :: thesis: for f, g being Element of Mor C st (SourceMap C) . g = (TargetMap C) . f holds
( (SourceMap C) . ((CompMap C) . (g,f)) = (SourceMap C) . f & (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g )
let f, g be Element of Mor C; :: thesis: ( (SourceMap C) . g = (TargetMap C) . f implies ( (SourceMap C) . ((CompMap C) . (g,f)) = (SourceMap C) . f & (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g ) )
assume A1: (SourceMap C) . g = (TargetMap C) . f ; :: thesis: ( (SourceMap C) . ((CompMap C) . (g,f)) = (SourceMap C) . f & (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g )

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

suppose A2: C is empty ; :: thesis: ( (SourceMap C) . ((CompMap C) . (g,f)) = (SourceMap C) . f & (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g )

thus (SourceMap C) . ((CompMap C) . (g,f)) = {} by A2
.= (SourceMap C) . f by A2 ; :: thesis: (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g
thus (TargetMap C) . ((CompMap C) . (g,f)) = {} by A2
.= (TargetMap C) . g by A2 ; :: thesis: verum

end;

suppose A3: not C is empty ; :: thesis: ( (SourceMap C) . ((CompMap C) . (g,f)) = (SourceMap C) . f & (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g )

then A4: [g,f] in dom (CompMap C) by A1, Th37;
then A5: (CompMap C) . [g,f] in rng (CompMap C) by FUNCT_1:3;
reconsider a = (CompMap C) . (g,f) as Element of Mor C by A5, BINOP_1:def 1;
consider d being morphism of C such that
A6: ( dom a = d & a |> d & d is identity ) by A3, Def18;
A7: g |> f by A4;
A8: a = the composition of C . [g,f] by BINOP_1:def 1
.= g (*) f by A4, Def2, Lm4 ;
then f |> d by A6, A7, Lm3;
then A9: dom a = dom f by A3, A6, Def18;
thus (SourceMap C) . ((CompMap C) . (g,f)) = dom a by A3, Def30
.= (SourceMap C) . f by A9, A3, Def30 ; :: thesis: (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g
consider c being morphism of C such that
A10: ( cod a = c & c |> a & c is identity ) by A3, Def19;
c |> g by A10, A7, A8, Lm3;
then A11: cod a = cod g by A3, A10, Def19;
thus (TargetMap C) . ((CompMap C) . (g,f)) = cod a by A3, Def31
.= (TargetMap C) . g by A11, A3, Def31 ; :: thesis: verum

end;

end;