let V be non empty set ; :: thesis: for f, g being Morphism of (Ens V) st dom g = cod f holds
g (*) f = (@ g) * (@ f)
let f, g 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 Def9;
then A2: dom (@ g) = cod (@ f) by Def10;
thus g (*) f = the Comp of (Ens V) . ((@ g),f) by A1, CAT_1:16
.= (@ g) * (@ f) by A2, Def11 ; :: thesis: verum