reconsider H1 = <^o1,o2^>, H2 = <^o2,o3^> as non empty set by A1;

reconsider F = the Comp of C . (o1,o2,o3) as Function of [:H2,H1:],<^o1,o3^> ;

reconsider y = g as Element of H2 ;

reconsider x = f as Element of H1 ;

F . (y,x) is Element of <^o1,o3^> ;

hence ( the Comp of C . (o1,o2,o3)) . (g,f) is Morphism of o1,o3 ; :: thesis: verum

reconsider F = the Comp of C . (o1,o2,o3) as Function of [:H2,H1:],<^o1,o3^> ;

reconsider y = g as Element of H2 ;

reconsider x = f as Element of H1 ;

F . (y,x) is Element of <^o1,o3^> ;

hence ( the Comp of C . (o1,o2,o3)) . (g,f) is Morphism of o1,o3 ; :: thesis: verum