let C be composable with_identities CategoryStr ; 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; ( (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
; ( (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 A3:
not
C is
empty
;
( (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
;
(TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . gconsider 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
;
verum end;