let C, D be Category; :: thesis: for f, f9 being Morphism of C
for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod 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 = cod f & dom g9 = cod g holds
[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
let g, g9 be Morphism of D; :: thesis: ( dom f9 = cod f & dom g9 = cod g implies [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)] )
assume that
A1: dom f9 = cod f and
A2: dom g9 = cod g ; :: thesis: [f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]
A3: ( [f9,f] in dom the Comp of C & [g9,g] in dom the Comp of D ) by A1, A2, CAT_1:15;
( dom [f9,g9] = [(dom f9),(dom g9)] & cod [f,g] = [(cod f),(cod g)] ) by Th22;
hence [f9,g9] (*) [f,g] = |: the Comp of C, the Comp of D:| . ([f9,g9],[f,g]) by A1, A2, CAT_1:16
.= [( the Comp of C . (f9,f)),( the Comp of D . (g9,g))] by A3, FUNCT_4:def 3
.= [(f9 (*) f),( the Comp of D . (g9,g))] by A1, CAT_1:16
.= [(f9 (*) f),(g9 (*) g)] by A2, CAT_1:16 ;
:: thesis: verum