let C, D be Category; :: thesis: for f, f9 being Morphism of C
for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds
[f9,g9] * [f,g] = [(f9 * f),(g9 * g)]
let f, f9 be Morphism of C; :: thesis: for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds
[f9,g9] * [f,g] = [(f9 * f),(g9 * g)]
let g, g9 be Morphism of D; :: thesis: ( dom f9 = cod f & dom g9 = cod g implies [f9,g9] * [f,g] = [(f9 * f),(g9 * g)] )
assume that
A1: dom f9 = cod f and
A2: dom g9 = cod g ; :: thesis: [f9,g9] * [f,g] = [(f9 * f),(g9 * g)]
A3: ( [f9,f] in dom the Comp of C & [g9,g] in dom the Comp of D ) by A1, A2, CAT_1:40;
( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th38;
hence [f9,g9] * [f,g] = |:the Comp of C,the Comp of D:| . [f9,g9],[f,g] by A1, A2, CAT_1:41
.= [(the Comp of C . f9,f),(the Comp of D . g9,g)] by A3, FUNCT_4:def 3
.= [(f9 * f),(the Comp of D . g9,g)] by A1, CAT_1:41
.= [(f9 * f),(g9 * g)] by A2, CAT_1:41 ;
:: thesis: verum