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