let F be Field; :: thesis: for a, c being Element of F

for b being Element of NonZero F holds

( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )

let a, c be Element of F; :: thesis: for b being Element of NonZero F holds

( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )

let b be Element of NonZero F; :: thesis: ( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )

set d = 1. F;

A1: (omf F) . (c,(1. F)) = c * (1. F)

.= c by REALSET2:21 ;

A2: (omf F) . (b,a) = b * a

.= a * b

.= (omf F) . (a,b) ;

( (ovf F) . (a,(1. F)) = a & 1. F is Element of NonZero F ) by Th27, STRUCT_0:2;

hence ( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a ) by A1, A2, Th25; :: thesis: verum

for b being Element of NonZero F holds

( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )

let a, c be Element of F; :: thesis: for b being Element of NonZero F holds

( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )

let b be Element of NonZero F; :: thesis: ( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )

set d = 1. F;

A1: (omf F) . (c,(1. F)) = c * (1. F)

.= c by REALSET2:21 ;

A2: (omf F) . (b,a) = b * a

.= a * b

.= (omf F) . (a,b) ;

( (ovf F) . (a,(1. F)) = a & 1. F is Element of NonZero F ) by Th27, STRUCT_0:2;

hence ( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a ) by A1, A2, Th25; :: thesis: verum