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