for C, D being Category holds
( the carrier of [:C,D:] = [: the carrier of C, the carrier of D:] & the carrier' of [:C,D:] = [: the carrier' of C, the carrier' of D:] & the Source of [:C,D:] = [: the Source of C, the Source of D:] & the Target of [:C,D:] = [: the Target of C, the Target of D:] & the Comp of [:C,D:] = |: the Comp of C, the Comp of D:| ) ;