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