let C, D be Category; :: thesis: for f, f' being Morphism of
for g, g' being Morphism of st dom f' = cod f & dom g' = cod g holds
[f',g'] * [f,g] = [(f' * f),(g' * g)]
let f, f' be Morphism of ; :: thesis: for g, g' being Morphism of st dom f' = cod f & dom g' = cod g holds
[f',g'] * [f,g] = [(f' * f),(g' * g)]
let g, g' be Morphism of ; :: thesis: ( dom f' = cod f & dom g' = cod g implies [f',g'] * [f,g] = [(f' * f),(g' * g)] )
assume that
A1: dom f' = cod f and
A2: dom g' = cod g ; :: thesis: [f',g'] * [f,g] = [(f' * f),(g' * g)]
A3: ( [f',f] in dom the Comp of C & [g',g] in dom the Comp of D ) by A1, A2, CAT_1:40;
( dom [f',g'] = [(dom f'),(dom g')] & cod [f,g] = [(cod f),(cod g)] ) by Th38;
hence [f',g'] * [f,g] = |:the Comp of C,the Comp of D:| . [f',g'],[f,g] by A1, A2, CAT_1:41
.= [(the Comp of C . f',f),(the Comp of D . g',g)] by A3, FUNCT_4:def 3
.= [(f' * f),(the Comp of D . g',g)] by A1, CAT_1:41
.= [(f' * f),(g' * g)] by A2, CAT_1:41 ;
:: thesis: verum