let C be Category; :: thesis: for f being Morphism of C
for g being morphism of (alter C) st f = g holds
( dom g = id (dom f) & cod g = id (cod f) )
let f be Morphism of C; :: thesis: for g being morphism of (alter C) st f = g holds
( dom g = id (dom f) & cod g = id (cod f) )
let g be morphism of (alter C); :: thesis: ( f = g implies ( dom g = id (dom f) & cod g = id (cod f) ) )
assume A1: f = g ; :: thesis: ( dom g = id (dom f) & cod g = id (cod f) )
A2: alter C = CategoryStr(# the carrier' of C, the Comp of C #) by CAT_6:def 34;
consider d1 being morphism of (alter C) such that
A3: ( dom g = d1 & g |> d1 & d1 is identity ) by CAT_6:def 18;
reconsider d11 = d1 as Morphism of C by A2, CAT_6:def 1;
[d1,d1] in dom the composition of (alter C) by A3, CAT_6:24, CAT_6:def 2;
then A4: dom d11 = cod d11 by A2, CAT_1:def 6;
reconsider d2 = id (dom f) as morphism of (alter C) by A2, CAT_6:def 1;
A5: d1 is left_identity by A3, CAT_6:def 14;
A6: for f1 being morphism of (alter C) st f1 |> d2 holds
f1 (*) d2 = f1

proof

let f1 be morphism of (alter C); :: thesis: ( f1 |> d2 implies f1 (*) d2 = f1 )
reconsider f11 = f1 as Morphism of C by A2, CAT_6:def 1;
assume f1 |> d2 ; :: thesis: f1 (*) d2 = f1
then A7: [f11,(id (dom f))] in dom the Comp of C by A2, CAT_6:def 2;
then A8: dom f11 = cod (id (dom f)) by CAT_1:def 6;
thus f1 (*) d2 = f11 (*) (id (dom f)) by A7, CAT_6:40
.= f1 by A8, CAT_1:22 ; :: thesis: verum

end;

[f,d11] in dom the Comp of C by A1, A2, A3, CAT_6:def 2;
then dom d11 = cod (id (dom f)) by A4, CAT_1:def 6;
then A9: [d1,d2] in dom the composition of (alter C) by A2, CAT_1:def 6;
A10: d1 = d1 (*) d2 by A9, A6, CAT_6:def 2
.= d2 by A9, A5, CAT_6:def 2, CAT_6:def 4 ;
thus dom g = id (dom f) by A3, A10; :: thesis: cod g = id (cod f)
consider c1 being morphism of (alter C) such that
A11: ( cod g = c1 & c1 |> g & c1 is identity ) by CAT_6:def 19;
reconsider c11 = c1 as Morphism of C by A2, CAT_6:def 1;
reconsider c2 = id (cod f) as morphism of (alter C) by A2, CAT_6:def 1;
A12: c1 is left_identity by A11, CAT_6:def 14;
A13: for f1 being morphism of (alter C) st f1 |> c2 holds
f1 (*) c2 = f1

proof

let f1 be morphism of (alter C); :: thesis: ( f1 |> c2 implies f1 (*) c2 = f1 )
reconsider f11 = f1 as Morphism of C by A2, CAT_6:def 1;
assume f1 |> c2 ; :: thesis: f1 (*) c2 = f1
then A14: [f11,(id (cod f))] in dom the Comp of C by A2, CAT_6:def 2;
then A15: dom f11 = cod (id (cod f)) by CAT_1:def 6;
thus f1 (*) c2 = f11 (*) (id (cod f)) by A14, CAT_6:40
.= f1 by A15, CAT_1:22 ; :: thesis: verum

end;

[c11,f] in dom the Comp of C by A1, A2, A11, CAT_6:def 2;
then dom c11 = cod (id (cod f)) by CAT_1:def 6;
then A16: [c11,(id (cod f))] in dom the Comp of C by CAT_1:def 6;
A17: c1 = c1 (*) c2 by A16, A2, A13, CAT_6:def 2
.= c2 by A16, A2, A12, CAT_6:def 2, CAT_6:def 4 ;
thus cod g = id (cod f) by A11, A17; :: thesis: verum