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, Th6;
then consider a being Element of Q. I such that
A2: ( a in u & (x `1 ) * (a `2 ) = (x `2 ) * (- (a `1 )) ) by Def10;
A3: a `2 <> 0. I by Th2;
consider y being Element of Q. I such that
A4: u = QClass. y by Def5;
y in u by A4, Th6;
then A5: (y `1 ) * (a `2 ) = (a `1 ) * (y `2 ) by A2, Th8;
A6: qadd u,(qaddinv u) = QClass. (padd y,x) by A1, A4, Th11;
( x `2 <> 0. I & y `2 <> 0. I ) by Th2;
then (x `2 ) * (y `2 ) <> 0. I by VECTSP_2:def 5;
then reconsider t = [(((y `1 ) * (x `2 )) + ((x `1 ) * (y `2 ))),((x `2 ) * (y `2 ))] as Element of Q. I by Def1;
A7: t `1 = 0. I

proof

(t `1 ) * (a `2 ) = (((y `1 ) * (x `2 )) + ((x `1 ) * (y `2 ))) * (a `2 ) by MCART_1:def 1
.= (((y `1 ) * (x `2 )) * (a `2 )) + (((x `1 ) * (y `2 )) * (a `2 )) by VECTSP_1:def 12
.= ((x `2 ) * ((a `1 ) * (y `2 ))) + (((x `1 ) * (y `2 )) * (a `2 )) by A5, GROUP_1:def 4
.= ((x `2 ) * ((a `1 ) * (y `2 ))) + (((x `2 ) * (- (a `1 ))) * (y `2 )) by A2, GROUP_1:def 4
.= ((x `2 ) * ((a `1 ) * (y `2 ))) + ((- ((x `2 ) * (a `1 ))) * (y `2 )) by GCD_1:51
.= ((x `2 ) * ((a `1 ) * (y `2 ))) + (- (((x `2 ) * (a `1 )) * (y `2 ))) by GCD_1:51
.= (((x `2 ) * (a `1 )) * (y `2 )) + (- (((x `2 ) * (a `1 )) * (y `2 ))) by GROUP_1:def 4
.= 0. I by RLVECT_1:def 11 ;
hence t `1 = 0. I by A3, VECTSP_2:def 5; :: thesis: verum

end;

A8: t `2 <> 0. I by Th2;
A9: 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 A10: (z `1 ) * (t `2 ) = (z `2 ) * (t `1 ) by Def4;
(z `2 ) * (t `1 ) = 0. I by A7, VECTSP_1:39;
then z `1 = 0. I by A8, A10, VECTSP_2:def 5;
hence z in q0. I by Def8; :: thesis: verum

end;

A11: 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 A12: z in q0. I ; :: thesis: z in QClass. t
A13: (z `2 ) * (t `1 ) = 0. I by A7, VECTSP_1:39;
z `1 = 0. I by A12, Def8;
then (z `1 ) * (t `2 ) = 0. I by VECTSP_1:39;
hence z in QClass. t by A13, Def4; :: thesis: verum

end;

qadd (qaddinv u),u = QClass. (padd x,y) by A1, A4, Th11;
hence ( qadd u,(qaddinv u) = q0. I & qadd (qaddinv u),u = q0. I ) by A6, A9, A11, SUBSET_1:8; :: thesis: verum