let F be Field; :: thesis: for a being Element of NonZero F
for b, c being Element of F holds
( (omf F) . a,b = c iff (ovf F) . c,a = b )
let a be Element of NonZero F; :: thesis: for b, c being Element of F holds
( (omf F) . a,b = c iff (ovf F) . c,a = b )
let b, c be Element of F; :: thesis: ( (omf F) . a,b = c iff (ovf F) . c,a = b )
set d = 1. F;
A1: (omf F) . c,(1. F) = c * (1. F)
.= c by REALSET2:25 ;
( 1. F is Element of NonZero F & (ovf F) . b,(1. F) = b ) by Th39, STRUCT_0:2;
hence ( (omf F) . a,b = c iff (ovf F) . c,a = b ) by A1, Th37; :: thesis: verum