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