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