let I be non degenerated commutative domRing-like Ring; for u being Element of Quot. I st u <> q0. I holds
( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I )
let u be Element of Quot. I; ( u <> q0. I implies ( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I ) )
assume A1:
u <> q0. I
; ( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I )
consider x being Element of Q. I such that
A2:
qmultinv u = QClass. x
by Def5;
consider y being Element of Q. I such that
A3:
u = QClass. y
by Def5;
( x `2 <> 0. I & y `2 <> 0. I )
by Th2;
then A4:
(x `2) * (y `2) <> 0. I
by VECTSP_2:def 1;
then reconsider t = [((x `1) * (y `1)),((x `2) * (y `2))] as Element of Q. I by Def1;
x in qmultinv u
by A2, Th5;
then consider a being Element of Q. I such that
A5:
a in u
and
A6:
(x `1) * (a `1) = (x `2) * (a `2)
by A1, Def11;
y in u
by A3, Th5;
then A7:
(y `1) * (a `2) = (a `1) * (y `2)
by A5, Th7;
A8:
a `1 <> 0. I
A9:
a `2 <> 0. I
by Th2;
A10:
for z being Element of Q. I st z in q1. I holds
z in QClass. t
A12:
for z being Element of Q. I st z in QClass. t holds
z in q1. I
( qmult (u,(qmultinv u)) = QClass. (pmult (y,x)) & qmult ((qmultinv u),u) = QClass. (pmult (x,y)) )
by A2, A3, Th10;
hence
( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I )
by A12, A10, SUBSET_1:3; verum