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 Th8; :: thesis: verum