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 ; :: thesis: verum