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

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