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 Th22;
then ( dom f9 = cod f & dom g9 = cod g ) by A1, XTUPLE_0:1;
hence [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] by Th23; :: thesis: verum