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

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