let V be non empty set ; :: thesis: for g, f being Morphism of (Ens V) st dom g = cod f holds
g * f = (@ g) * (@ f)
let g, f be Morphism of (Ens V); :: thesis: ( dom g = cod f implies g * f = (@ g) * (@ f) )
assume A1: dom g = cod f ; :: thesis: g * f = (@ g) * (@ f)
then dom (@ g) = cod f by Def10;
then A2: dom (@ g) = cod (@ f) by Def11;
thus g * f = the Comp of (Ens V) . ((@ g),f) by A1, CAT_1:16
.= (@ g) * (@ f) by A2, Def12 ; :: thesis: verum