let C be non empty composable with_identities CategoryStr ; :: thesis: for f, g being Element of Mor C holds
( [g,f] in dom (CompMap C) iff (SourceMap C) . g = (TargetMap C) . f )
let f, g be Element of Mor C; :: thesis: ( [g,f] in dom (CompMap C) iff (SourceMap C) . g = (TargetMap C) . f )
hereby :: thesis: ( (SourceMap C) . g = (TargetMap C) . f implies [g,f] in dom (CompMap C) )
assume [g,f] in dom (CompMap C) ; :: thesis: (SourceMap C) . g = (TargetMap C) . f
then A1: g |> f ;
consider u being morphism of C such that
A2: ( dom g = u & g |> u & u is identity ) by Def18;
g (*) u = g by A2, Def5;
then A3: u |> f by A2, A1, Lm3;
thus (SourceMap C) . g = dom g by Def30
.= cod f by A3, A2, Def19
.= (TargetMap C) . f by Def31 ; :: thesis: verum
end;
assume A4: (SourceMap C) . g = (TargetMap C) . f ; :: thesis: [g,f] in dom (CompMap C)
A5: dom g = (SourceMap C) . g by Def30
.= cod f by A4, Def31 ;
consider d being morphism of C such that
A6: ( dom g = d & g |> d & d is identity ) by Def18;
consider c being morphism of C such that
A7: ( cod f = c & c |> f & c is identity ) by Def19;
g (*) d |> f by A6, A7, A5, Lm3;
hence [g,f] in dom (CompMap C) by A6, Def5; :: thesis: verum