theorem
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:| ) ;