let C be associative composable with_identities CategoryStr ; for f, g, h being Element of Mor C st (SourceMap C) . h = (TargetMap C) . g & (SourceMap C) . g = (TargetMap C) . f holds
(CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)
let f, g, h be Element of Mor C; ( (SourceMap C) . h = (TargetMap C) . g & (SourceMap C) . g = (TargetMap C) . f implies (CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f) )
assume A1:
( (SourceMap C) . h = (TargetMap C) . g & (SourceMap C) . g = (TargetMap C) . f )
; (CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)
per cases
( C is empty or not C is empty )
;
suppose A3:
not
C is
empty
;
(CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)A4:
[h,g] in dom (CompMap C)
by Th37, A3, A1;
then A5:
h |> g
;
A6:
[g,f] in dom (CompMap C)
by Th37, A3, A1;
then A7:
g |> f
;
A8:
h |> g (*) f
by A7, A5, Lm3;
A9:
h (*) g |> f
by A7, A5, Lm3;
A10:
(CompMap C) . (
g,
f) =
the
composition of
C . [g,f]
by BINOP_1:def 1
.=
g (*) f
by A6, Def2, Lm4
;
A11:
(CompMap C) . (
h,
g) =
the
composition of
C . [h,g]
by BINOP_1:def 1
.=
h (*) g
by A4, Def2, Lm4
;
thus (CompMap C) . (
h,
((CompMap C) . (g,f))) =
(CompMap C) . [h,(g (*) f)]
by A10, BINOP_1:def 1
.=
h (*) (g (*) f)
by A8, Lm4
.=
(h (*) g) (*) f
by A5, A7, Lm5
.=
(CompMap C) . [(h (*) g),f]
by A9, Lm4
.=
(CompMap C) . (
((CompMap C) . (h,g)),
f)
by A11, BINOP_1:def 1
;
verum end; end;