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