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 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 5;
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, Th6;
then A6: (y `1 ) * (a `2 ) = (a `1 ) * (y `2 ) by A2, Th8;
(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 A6, GROUP_1:def 4
.= ((x `2 ) * ((a `1 ) * (y `2 ))) + (((x `2 ) * (- (a `1 ))) * (y `2 )) by A3, 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 ;
then A7: t `1 = 0. I by A5, VECTSP_2:def 5;
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 by VECTSP_1:39;
(z `2 ) * (t `1 ) = 0. I by A7, VECTSP_1:39;
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, VECTSP_1:39;
then z `1 = 0. I by A10, A12, VECTSP_2:def 5;
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, Th11;
hence ( qadd u,(qaddinv u) = q0. I & qadd (qaddinv u),u = q0. I ) by A11, A8, SUBSET_1:8; :: thesis: verum