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:21 ;
( 1. F is Element of NonZero F & (ovf F) . (b,(1. F)) = b ) by Th27, STRUCT_0:2;
hence ( (omf F) . (a,b) = c iff (ovf F) . (c,a) = b ) by A1, Th25; :: thesis: verum