let F be Field; for a, c being Element of F
for b, d being Element of NonZero F holds
( (ovf F) . (a,b) = (ovf F) . (c,d) iff (omf F) . (a,d) = (omf F) . (b,c) )
let a, c be Element of F; for b, d being Element of NonZero F holds
( (ovf F) . (a,b) = (ovf F) . (c,d) iff (omf F) . (a,d) = (omf F) . (b,c) )
let b, d be Element of NonZero F; ( (ovf F) . (a,b) = (ovf F) . (c,d) iff (omf F) . (a,d) = (omf F) . (b,c) )
( (ovf F) . (a,b) = (omf F) . (a,((revf F) . b)) & (ovf F) . (c,d) = (omf F) . (c,((revf F) . d)) )
by Def2;
hence
( (ovf F) . (a,b) = (ovf F) . (c,d) iff (omf F) . (a,d) = (omf F) . (b,c) )
by Th5; verum