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;

now

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:

proof

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:43;
hence ( [g,f] in dom (~ the Comp of C) iff the Target of C . g = the Source of C . f ) by CAT_1:def 8; :: 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

proof

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:44; :: 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:

proof

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 8; :: 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:

proof

let f, g, h be Element of the carrier' of C; :: thesis:
assume A4: ( the Target of C . h = the Source of C . g & the Target of C . g = the Source of C . f ) ; :: thesis:
then ( [g,f] in dom (~ the Comp of C) & [h,g] in dom (~ the Comp of C) ) by A1;
then ( (~ the Comp of C) . g,f = the Comp of C . f,g & (~ the Comp of C) . h,g = the Comp of C . g,h & the Source of C . ((~ the Comp of C) . g,f) = the Source of C . g & the Target of C . ((~ the Comp of C) . h,g) = the Target of C . g & (~ the Comp of C) . g,f is Element of the carrier' of C & (~ the Comp of C) . h,g is Element of the carrier' of C ) by A2, A3, A4, PARTFUN1:27;
then ( (~ the Comp of C) . h,((~ the Comp of C) . g,f) = the Comp of C . (the Comp of C . f,g),h & (~ the Comp of C) . ((~ the Comp of C) . h,g),f = the Comp of C . f,(the Comp of C . g,h) ) by A2, A4;
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, CAT_1:def 8; :: thesis:

end;

let b be Element of the carrier of C; :: thesis:
thus A5: ( the Target of C . (the Id of C . b) = b & the Source of C . (the Id of C . b) = b ) by CAT_1:def 8; :: 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:

proof

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, A5;
hence ( the Source of C . f = b implies (~ the Comp of C) . (the Id of C . b),f = f ) by CAT_1:def 8; :: 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, A5;
hence ( the Target of C . g = b implies (~ the Comp of C) . g,(the Id of C . b) = g ) by CAT_1:def 8; :: 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 8; :: thesis: