let F be Field; :: thesis: for a, c being Element of F
for b, d being Element of NonZero F holds
( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) iff (omf F) . a,d = (omf F) . b,c )
let a, c be Element of F; :: thesis: for b, d being Element of NonZero F holds
( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) iff (omf F) . a,d = (omf F) . b,c )
let b, d be Element of NonZero F; :: thesis: ( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) iff (omf F) . a,d = (omf F) . b,c )
A1: ( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) implies (omf F) . a,d = (omf F) . b,c )

proof

reconsider revfb = (revf F) . b, revfd = (revf F) . d as Element of NonZero F ;
reconsider crevfd = c * revfd as Element of F ;
assume A2: (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) ; :: thesis: (omf F) . a,d = (omf F) . b,c
A3: c = c * (1. F) by REALSET2:25
.= (omf F) . c,(d * revfd) by REALSET2:def 18
.= c * (revfd * d)
.= (c * revfd) * d by REALSET2:23 ;
a = a * (1. F) by REALSET2:25
.= (omf F) . a,(b * revfb) by REALSET2:def 18
.= a * (revfb * b)
.= (a * revfb) * b by REALSET2:23
.= b * crevfd by A2
.= (omf F) . b,((omf F) . c,((revf F) . d)) ;
hence (omf F) . a,d = (b * (c * revfd)) * d
.= b * ((c * revfd) * d) by REALSET2:23
.= (omf F) . b,c by A3 ;
:: thesis: verum

end;

( (omf F) . a,d = (omf F) . b,c implies (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) )

proof

reconsider revfd = (revf F) . d, revfb = (revf F) . b as Element of NonZero F ;
reconsider crevfd = (omf F) . c,revfd as Element of F ;
assume A4: (omf F) . a,d = (omf F) . b,c ; :: thesis: (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d)
a = a * (1. F) by REALSET2:25
.= (omf F) . a,(1. F)
.= a * (d * revfd) by REALSET2:def 18
.= (a * d) * revfd by REALSET2:23
.= (b * c) * revfd by A4
.= b * (c * revfd) by REALSET2:23
.= crevfd * b ;
hence (omf F) . a,((revf F) . b) = (crevfd * b) * revfb
.= crevfd * (b * revfb) by REALSET2:23
.= ((omf F) . c,revfd) * (1. F) by REALSET2:def 18
.= (omf F) . c,((revf F) . d) by REALSET2:25 ;
:: thesis: verum

end;

hence ( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) iff (omf F) . a,d = (omf F) . b,c ) by A1; :: thesis: verum