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:21
.= (omf F) . (c,(d * revfd)) by REALSET2:def 6
.= c * (revfd * d)
.= (c * revfd) * d by REALSET2:19 ;
a = a * (1. F) by REALSET2:21
.= (omf F) . (a,(b * revfb)) by REALSET2:def 6
.= a * (revfb * b)
.= (a * revfb) * b by REALSET2:19
.= 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:19
.= (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:21
.= (omf F) . (a,(1. F))
.= a * (d * revfd) by REALSET2:def 6
.= (a * d) * revfd by REALSET2:19
.= (b * c) * revfd by A4
.= b * (c * revfd) by REALSET2:19
.= crevfd * b ;
hence (omf F) . (a,((revf F) . b)) = (crevfd * b) * revfb
.= crevfd * (b * revfb) by REALSET2:19
.= ((omf F) . (c,revfd)) * (1. F) by REALSET2:def 6
.= (omf F) . (c,((revf F) . d)) by REALSET2:21 ;
:: 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