let C, D be Category; :: thesis: for f being Morphism of C
for g being Morphism of D holds
( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )
let f be Morphism of C; :: thesis: for g being Morphism of D holds
( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )
let g be Morphism of D; :: thesis: ( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )
thus dom [f,g] = [: the Source of C, the Source of D:] . (f,g)
.= [(dom f),(dom g)] by FUNCT_3:75 ; :: thesis: cod [f,g] = [(cod f),(cod g)]
thus cod [f,g] = [: the Target of C, the Target of D:] . (f,g)
.= [(cod f),(cod g)] by FUNCT_3:75 ; :: thesis: verum