reconsider A = <^o1,o2^>, B = <^(F . o2),(F . o1)^> as non empty set by A1, A2;
reconsider M = Morph-Map (F,o1,o2) as Function of A,B ;
reconsider m = m as Element of A ;
M . m is Element of B ;
hence (Morph-Map (F,o1,o2)) . m is Morphism of (F . o2),(F . o1) ; :: thesis: verum