let F be Field; :: thesis: for a being Element of the carrier of F \ {(0. F)}
for b, c being Element of the carrier of F holds
( (omf F) . a,b = c iff (ovf F) . c,a = b )
let a be Element of the carrier of F \ {(0. F)}; :: thesis: for b, c being Element of the carrier of F holds
( (omf F) . a,b = c iff (ovf F) . c,a = b )
let b, c be Element of the carrier of F; :: thesis: ( (omf F) . a,b = c iff (ovf F) . c,a = b )
set d = 1. F;
A1: 1. F is Element of the carrier of F \ {(0. F)} by REALSET2:31;
A2: (omf F) . c,(1. F) = c * (1. F)
.= c by REALSET2:25 ;
(ovf F) . b,(1. F) = b by Th39;
hence ( (omf F) . a,b = c iff (ovf F) . c,a = b ) by A1, A2, Th37; :: thesis: verum