let C be non empty non void CatStr ; :: thesis:
set CP = the Comp of C;
set CD = the Source of C;
set CC = the Target of C;
set CI = the Id of C;
assume that
A1: for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f ) and
A2: for f, g being Morphism of C st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g ) and
A3: for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f and
A4: for b being Object of C holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of C st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of C st dom g = b holds
g * (id b) = g ) ) ; :: thesis:
thus A5: for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) :: according to CAT_1:def 5 :: thesis:

let f, g be Element of the carrier' of C; :: thesis:
( the Source of C . g = dom g & the Target of C . f = cod f ) ;
hence ( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) by A1; :: thesis:

end;

thus A6: for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . ( the Comp of C . (g,f)) = the Source of C . f & the Target of C . ( the Comp of C . (g,f)) = the Target of C . g ) :: thesis:

let f, g be Element of the carrier' of C; :: thesis:
assume A7: the Source of C . g = the Target of C . f ; :: thesis:
( the Source of C . g = dom g & the Target of C . f = cod f ) ;
then A8: ( dom (g * f) = dom f & cod (g * f) = cod g ) by A2, A7;
[g,f] in dom the Comp of C by A5, A7;
hence ( the Source of C . ( the Comp of C . (g,f)) = the Source of C . f & the Target of C . ( the Comp of C . (g,f)) = the Target of C . g ) by A8, Def4; :: thesis:

end;

thus for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . (h,( the Comp of C . (g,f))) = the Comp of C . (( the Comp of C . (h,g)),f) :: thesis:

let f, g, h be Element of the carrier' of C; :: thesis:
assume that
A9: the Source of C . h = the Target of C . g and
A10: the Source of C . g = the Target of C . f ; :: thesis:
A11: ( the Source of C . g = dom g & the Target of C . f = cod f ) ;
[g,f] in dom the Comp of C by A5, A10;
then A12: g * f = the Comp of C . (g,f) by Def4;
[h,g] in dom the Comp of C by A5, A9;
then A13: h * g = the Comp of C . (h,g) by Def4;
the Target of C . ( the Comp of C . (g,f)) = the Target of C . g by A6, A10;
then [h,(g * f)] in dom the Comp of C by A5, A9, A12;
then A14: the Comp of C . (h,(g * f)) = h * (g * f) by Def4;
the Source of C . ( the Comp of C . (h,g)) = the Source of C . g by A6, A9;
then [(h * g),f] in dom the Comp of C by A5, A10, A13;
then A15: the Comp of C . ((h * g),f) = (h * g) * f by Def4;
( the Source of C . h = dom h & the Target of C . g = cod g ) ;
hence the Comp of C . (h,( the Comp of C . (g,f))) = the Comp of C . (( the Comp of C . (h,g)),f) by A3, A9, A10, A11, A12, A13, A14, A15; :: thesis:

end;

let b be Element of C; :: thesis:
( dom (id b) = b & cod (id b) = b ) by A4;
hence ( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b ) ; :: thesis:
thus for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f :: thesis:

let f be Element of the carrier' of C; :: thesis:
assume A16: the Target of C . f = b ; :: thesis:
the Target of C . f = cod f ;
then A17: (id b) * f = f by A4, A16;
dom (id b) = b by A4;
then [( the Id of C . b),f] in dom the Comp of C by A5, A16;
hence the Comp of C . (( the Id of C . b),f) = f by A17, Def4; :: thesis:

end;

let g be Element of the carrier' of C; :: thesis:
assume A18: the Source of C . g = b ; :: thesis:
the Source of C . g = dom g ;
then A19: g * (id b) = g by A4, A18;
cod (id b) = b by A4;
then [g,( the Id of C . b)] in dom the Comp of C by A5, A18;
hence the Comp of C . (g,( the Id of C . b)) = g by A19, Def4; :: thesis: