let I be non degenerated commutative domRing-like Ring; for u being Element of Quot. I holds
( qadd (u,(qaddinv u)) = q0. I & qadd ((qaddinv u),u) = q0. I )
let u be Element of Quot. I; ( qadd (u,(qaddinv u)) = q0. I & qadd ((qaddinv u),u) = q0. I )
consider x being Element of Q. I such that
A1:
qaddinv u = QClass. x
by Def5;
x in qaddinv u
by A1, Th5;
then consider a being Element of Q. I such that
A2:
a in u
and
A3:
(x `1) * (a `2) = (x `2) * (- (a `1))
by Def10;
consider y being Element of Q. I such that
A4:
u = QClass. y
by Def5;
( x `2 <> 0. I & y `2 <> 0. I )
by Th2;
then
(x `2) * (y `2) <> 0. I
by VECTSP_2:def 1;
then reconsider t = [(((y `1) * (x `2)) + ((x `1) * (y `2))),((x `2) * (y `2))] as Element of Q. I by Def1;
A5:
a `2 <> 0. I
by Th2;
y in u
by A4, Th5;
then A6:
(y `1) * (a `2) = (a `1) * (y `2)
by A2, Th7;
(t `1) * (a `2) =
(((y `1) * (x `2)) + ((x `1) * (y `2))) * (a `2)
.=
(((y `1) * (x `2)) * (a `2)) + (((x `1) * (y `2)) * (a `2))
by VECTSP_1:def 3
.=
((x `2) * ((a `1) * (y `2))) + (((x `1) * (y `2)) * (a `2))
by A6, GROUP_1:def 3
.=
((x `2) * ((a `1) * (y `2))) + (((x `2) * (- (a `1))) * (y `2))
by A3, GROUP_1:def 3
.=
((x `2) * ((a `1) * (y `2))) + ((- ((x `2) * (a `1))) * (y `2))
by GCD_1:48
.=
((x `2) * ((a `1) * (y `2))) + (- (((x `2) * (a `1)) * (y `2)))
by GCD_1:48
.=
(((x `2) * (a `1)) * (y `2)) + (- (((x `2) * (a `1)) * (y `2)))
by GROUP_1:def 3
.=
0. I
by RLVECT_1:def 10
;
then A7:
t `1 = 0. I
by A5, VECTSP_2:def 1;
A8:
for z being Element of Q. I st z in q0. I holds
z in QClass. t
A10:
t `2 <> 0. I
by Th2;
A11:
for z being Element of Q. I st z in QClass. t holds
z in q0. I
( qadd (u,(qaddinv u)) = QClass. (padd (y,x)) & qadd ((qaddinv u),u) = QClass. (padd (x,y)) )
by A1, A4, Th9;
hence
( qadd (u,(qaddinv u)) = q0. I & qadd ((qaddinv u),u) = q0. I )
by A11, A8, SUBSET_1:3; verum