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