ex a, b being Element of o Hom ex f being Morphism of C st
( m = [[a,b],f] & dom f = cod a & f (*) a = b ) by Def12;
hence m `11 is Element of o Hom by MCART_1:85; :: thesis: verum