let I be non degenerated commutative domRing-like Ring; :: thesis: 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; :: thesis: ( 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

proof

let z be Element of Q. I; :: thesis: ( z in q0. I implies z in QClass. t )
assume z in q0. I ; :: thesis: z in QClass. t
then z `1 = 0. I by Def8;
then A9: (z `1) * (t `2) = 0. I ;
(z `2) * (t `1) = 0. I by A7;
hence z in QClass. t by A9, Def4; :: thesis: verum

end;

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

proof

let z be Element of Q. I; :: thesis: ( z in QClass. t implies z in q0. I )
assume z in QClass. t ; :: thesis: z in q0. I
then A12: (z `1) * (t `2) = (z `2) * (t `1) by Def4;
(z `2) * (t `1) = 0. I by A7;
then z `1 = 0. I by A10, A12, VECTSP_2:def 1;
hence z in q0. I by Def8; :: thesis: verum

end;

( 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; :: thesis: verum