consider a, b being Element of Hom o, f being Morphism of C such that
A3: ( m = [[a,b],f] & dom b = cod f & a = b * f ) by Def11;
thus m `12 is Element of Hom o by A3, MCART_1:89; :: thesis: verum