let I be non degenerated commutative domRing-like Ring; for u being Element of Quot. I holds
( (quotmult I) . (u,(q1. I)) = u & (quotmult I) . ((q1. I),u) = u )
let u be Element of Quot. I; ( (quotmult I) . (u,(q1. I)) = u & (quotmult I) . ((q1. I),u) = u )
A1: (quotmult I) . ((q1. I),u) =
qmult ((q1. I),u)
by Def13
.=
u
by Th14
;
(quotmult I) . (u,(q1. I)) =
qmult (u,(q1. I))
by Def13
.=
u
by Th14
;
hence
( (quotmult I) . (u,(q1. I)) = u & (quotmult I) . ((q1. I),u) = u )
by A1; verum