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