for F being Field
for a being Element of F
for b, c being Element of NonZero F holds (ovf F) . (a,((ovf F) . (b,c))) = (omf F) . (((ovf F) . (a,b)),c)