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

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