let C, D be Category; 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; 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; ( dom [f9,g9] = cod [f,g] implies [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] )
assume A1:
dom [f9,g9] = cod [f,g]
; [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; verum