let C, D be Category; :: thesis: for f, f' being Morphism of C
for g, g' being Morphism of D st dom [f',g'] = cod [f,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',g'] = cod [f,g] holds
[f',g'] * [f,g] = [(f' * f),(g' * g)]
let g, g' be Morphism of D; :: thesis: ( dom [f',g'] = cod [f,g] implies [f',g'] * [f,g] = [(f' * f),(g' * g)] )
assume A1: dom [f',g'] = cod [f,g] ; :: thesis: [f',g'] * [f,g] = [(f' * f),(g' * g)]
( [(dom f'),(dom g')] = dom [f',g'] & cod [f,g] = [(cod f),(cod g)] ) by Th38;
then ( dom f' = cod f & dom g' = cod g ) by A1, ZFMISC_1:33;
hence [f',g'] * [f,g] = [(f' * f),(g' * g)] by Th39; :: thesis: verum