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