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 `2 is Morphism of C by MCART_1:7; :: thesis: verum