let F be Field; :: thesis: 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; :: thesis: 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; :: thesis: ( (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; :: thesis: verum