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