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

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