let C, D be Category; :: thesis: for f being Morphism of
for g being Morphism of holds
( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )
let f be Morphism of ; :: thesis: for g being Morphism of holds
( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )
let g be Morphism of ; :: 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:96 ; :: 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:96 ; :: thesis: verum