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

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