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