let C be composable with_identities CategoryStr ; :: thesis: 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; :: thesis: ( (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 A1: C is empty ; :: thesis: ( (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 A2: b = {} by SUBSET_1:def 1;
thus (SourceMap C) . ((IdMap C) . b) = b by A1, A2; :: thesis: ( (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 ) )
thus (TargetMap C) . ((IdMap C) . b) = b by A1, A2; :: thesis: ( ( 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 :: thesis: for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g

proof

let f be Element of Mor C; :: thesis: ( (TargetMap C) . f = b implies (CompMap C) . (((IdMap C) . b),f) = f )
assume (TargetMap C) . f = b ; :: thesis: (CompMap C) . (((IdMap C) . b),f) = f
A3: f = {} by A1, SUBSET_1:def 1;
thus (CompMap C) . (((IdMap C) . b),f) = the composition of C . [((IdMap C) . b),f] by BINOP_1:def 1
.= f by A1, A3 ; :: thesis: verum

end;

thus for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g :: thesis: verum

proof

let g be Element of Mor C; :: thesis: ( (SourceMap C) . g = b implies (CompMap C) . (g,((IdMap C) . b)) = g )
assume (SourceMap C) . g = b ; :: thesis: (CompMap C) . (g,((IdMap C) . b)) = g
A4: g = {} by A1, SUBSET_1:def 1;
thus (CompMap C) . (g,((IdMap C) . b)) = the composition of C . [g,((IdMap C) . b)] by BINOP_1:def 1
.= g by A1, A4 ; :: thesis: verum

end;

end;

suppose A5: not C is empty ; :: thesis: ( (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; :: thesis: ( (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; :: thesis: ( ( 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 :: thesis: for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g

proof

let f be Element of Mor C; :: thesis: ( (TargetMap C) . f = b implies (CompMap C) . (((IdMap C) . b),f) = f )
assume (TargetMap C) . f = b ; :: thesis: (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 ; :: thesis: verum

end;

thus for g being Element of Mor C st (SourceMap C) . g = b holds
(CompMap C) . (g,((IdMap C) . b)) = g :: thesis: verum

proof

let g be Element of Mor C; :: thesis: ( (SourceMap C) . g = b implies (CompMap C) . (g,((IdMap C) . b)) = g )
assume (SourceMap C) . g = b ; :: thesis: (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 ; :: thesis: verum

end;

end;

end;