let C be Category; :: thesis:
set M = the carrier' of C;
set d = the Target of C;
set c = the Source of C;
set p = ~ the Comp of C;
set i = the Id of C;

thus A1: for f, g being Element of the carrier' of C holds
( [g,f] in dom (~ the Comp of C) iff the Target of C . g = the Source of C . f ) :: thesis:

let f, g be Element of the carrier' of C; :: thesis:
( [g,f] in dom (~ the Comp of C) iff [f,g] in dom the Comp of C ) by FUNCT_4:42;
hence ( [g,f] in dom (~ the Comp of C) iff the Target of C . g = the Source of C . f ) by CAT_1:def 5; :: thesis:

end;

A2: for f, g being Element of the carrier' of C st the Target of C . g = the Source of C . f holds
(~ the Comp of C) . (g,f) = the Comp of C . (f,g)

let f, g be Element of the carrier' of C; :: thesis:
assume the Target of C . g = the Source of C . f ; :: thesis:
then [g,f] in dom (~ the Comp of C) by A1;
hence (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by FUNCT_4:43; :: thesis:

end;

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

let f, g be Element of the carrier' of C; :: thesis:
( the Target of C . g = the Source of C . f implies (~ the Comp of C) . (g,f) = the Comp of C . (f,g) ) by A2;
hence ( the Target of C . g = the Source of C . f implies ( the Target of C . ((~ the Comp of C) . (g,f)) = the Target of C . f & the Source of C . ((~ the Comp of C) . (g,f)) = the Source of C . g ) ) by CAT_1:def 5; :: thesis:

end;

thus for f, g, h being Element of the carrier' of C st the Target of C . h = the Source of C . g & the Target of C . g = the Source 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
A4: the Target of C . h = the Source of C . g and
A5: the Target of C . g = the Source of C . f ; :: thesis:
[h,g] in dom (~ the Comp of C) by A1, A4;
then A6: (~ the Comp of C) . (h,g) is Element of the carrier' of C by PARTFUN1:4;
[g,f] in dom (~ the Comp of C) by A1, A5;
then A7: (~ the Comp of C) . (g,f) is Element of the carrier' of C by PARTFUN1:4;
( (~ the Comp of C) . (h,g) = the Comp of C . (g,h) & the Target of C . ((~ the Comp of C) . (h,g)) = the Target of C . g ) by A2, A3, A4;
then A8: (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) = the Comp of C . (f,( the Comp of C . (g,h))) by A2, A5, A6;
( (~ the Comp of C) . (g,f) = the Comp of C . (f,g) & the Source of C . ((~ the Comp of C) . (g,f)) = the Source of C . g ) by A2, A3, A5;
then (~ the Comp of C) . (h,((~ the Comp of C) . (g,f))) = the Comp of C . (( the Comp of C . (f,g)),h) by A2, A4, A7;
hence (~ the Comp of C) . (h,((~ the Comp of C) . (g,f))) = (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) by A4, A5, A8, CAT_1:def 5; :: thesis:

end;

let b be Element of the carrier of C; :: thesis:
thus A9: ( the Target of C . ( the Id of C . b) = b & the Source of C . ( the Id of C . b) = b ) by CAT_1:def 5; :: thesis:
thus for f being Element of the carrier' of C st the Source 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:
( the Source of C . f = b implies (~ the Comp of C) . (( the Id of C . b),f) = the Comp of C . (f,( the Id of C . b)) ) by A2, A9;
hence ( the Source of C . f = b implies (~ the Comp of C) . (( the Id of C . b),f) = f ) by CAT_1:def 5; :: thesis:

end;

let g be Element of the carrier' of C; :: thesis:
( the Target of C . g = b implies (~ the Comp of C) . (g,( the Id of C . b)) = the Comp of C . (( the Id of C . b),g) ) by A2, A9;
hence ( the Target of C . g = b implies (~ the Comp of C) . (g,( the Id of C . b)) = g ) by CAT_1:def 5; :: thesis:

end;

hence CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C), the Id of C #) is Category by CAT_1:def 5; :: thesis: