let C be composable with_identities CategoryStr ; for b being Element of Ob C holds
( (SourceMap C) . ((IdMap C) . b) = b & (TargetMap C) . ((IdMap C) . b) = b & ( for f being Element of Mor C st (TargetMap C) . f = b holds
(CompMap C) . (((IdMap C) . b),f) = f ) & ( for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g ) )
let b be Element of Ob C; ( (SourceMap C) . ((IdMap C) . b) = b & (TargetMap C) . ((IdMap C) . b) = b & ( for f being Element of Mor C st (TargetMap C) . f = b holds
(CompMap C) . (((IdMap C) . b),f) = f ) & ( for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g ) )
per cases
( C is empty or not C is empty )
;
suppose A5:
not
C is
empty
;
( (SourceMap C) . ((IdMap C) . b) = b & (TargetMap C) . ((IdMap C) . b) = b & ( for f being Element of Mor C st (TargetMap C) . f = b holds
(CompMap C) . (((IdMap C) . b),f) = f ) & ( for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g ) )then A6:
(IdMap C) . b =
id- b
by Def32
.=
b
;
not
Ob C is
empty
by A5;
then
b in Ob C
;
then reconsider u =
b as
Element of
Mor C ;
A7:
u is
identity
by A5, Th22;
consider d being
morphism of
C such that A8:
(
dom u = d &
u |> d &
d is
identity )
by A5, Def18;
A9:
d =
u (*) d
by A7, A8, Def4
.=
u
by A8, Def5
;
thus A10:
(SourceMap C) . ((IdMap C) . b) = b
by A8, A9, A6, A5, Def30;
( (TargetMap C) . ((IdMap C) . b) = b & ( for f being Element of Mor C st (TargetMap C) . f = b holds
(CompMap C) . (((IdMap C) . b),f) = f ) & ( for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g ) )consider c being
morphism of
C such that A11:
(
cod u = c &
c |> u &
c is
identity )
by A5, Def19;
A12:
c =
c (*) u
by A7, A11, Def5
.=
u
by A11, Def4
;
thus A13:
(TargetMap C) . ((IdMap C) . b) = b
by A11, A12, A6, A5, Def31;
( ( for f being Element of Mor C st (TargetMap C) . f = b holds
(CompMap C) . (((IdMap C) . b),f) = f ) & ( for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g ) )thus
for
f being
Element of
Mor C st
(TargetMap C) . f = b holds
(CompMap C) . (
((IdMap C) . b),
f)
= f
for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = gproof
let f be
Element of
Mor C;
( (TargetMap C) . f = b implies (CompMap C) . (((IdMap C) . b),f) = f )
assume
(TargetMap C) . f = b
;
(CompMap C) . (((IdMap C) . b),f) = f
then A14:
[u,f] in dom (CompMap C)
by A6, A10, A5, Th37;
then A15:
u |> f
;
thus (CompMap C) . (
((IdMap C) . b),
f) =
(CompMap C) . [u,f]
by A6, BINOP_1:def 1
.=
u (*) f
by A14, Def2, Lm4
.=
f
by A7, A15, Def4
;
verum
end; thus
for
g being
Element of
Mor C st
(SourceMap C) . g = b holds
(CompMap C) . (
g,
((IdMap C) . b))
= g
verumproof
let g be
Element of
Mor C;
( (SourceMap C) . g = b implies (CompMap C) . (g,((IdMap C) . b)) = g )
assume
(SourceMap C) . g = b
;
(CompMap C) . (g,((IdMap C) . b)) = g
then A16:
[g,u] in dom (CompMap C)
by A6, A13, A5, Th37;
then A17:
g |> u
;
thus (CompMap C) . (
g,
((IdMap C) . b)) =
(CompMap C) . [g,u]
by A6, BINOP_1:def 1
.=
g (*) u
by A16, Def2, Lm4
.=
g
by A7, A17, Def5
;
verum
end; end; end;