let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of Quot. I holds
( qadd u,(q0. I) = u & qadd (q0. I),u = u )
let u be Element of Quot. I; :: thesis: ( qadd u,(q0. I) = u & qadd (q0. I),u = u )
consider x being Element of Q. I such that
A1: q0. I = QClass. x by Def5;
consider y being Element of Q. I such that
A2: u = QClass. y by Def5;
A3: x `2 <> 0. I by Th2;
y `2 <> 0. I by Th2;
then (x `2 ) * (y `2 ) <> 0. I by A3, 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;
x in q0. I by A1, Th6;
then A4: x `1 = 0. I by Def8;
A5: for z being Element of Q. I st z in QClass. y holds
z in QClass. t

proof

let z be Element of Q. I; :: thesis: ( z in QClass. y implies z in QClass. t )
assume z in QClass. y ; :: thesis: z in QClass. t
then A6: (z `1 ) * (y `2 ) = (z `2 ) * (y `1 ) by Def4;
(z `1 ) * (t `2 ) = (z `1 ) * ((x `2 ) * (y `2 )) by MCART_1:def 2
.= ((z `2 ) * (y `1 )) * (x `2 ) by A6, GROUP_1:def 4
.= (z `2 ) * ((y `1 ) * (x `2 )) by GROUP_1:def 4
.= (z `2 ) * (((y `1 ) * (x `2 )) + (0. I)) by RLVECT_1:10
.= (z `2 ) * (((y `1 ) * (x `2 )) + ((x `1 ) * (y `2 ))) by A4, VECTSP_1:39
.= (z `2 ) * (t `1 ) by MCART_1:def 1 ;
hence z in QClass. t by Def4; :: thesis: verum

end;

A7: for z being Element of Q. I st z in QClass. t holds
z in QClass. y

proof

let z be Element of Q. I; :: thesis: ( z in QClass. t implies z in QClass. y )
x `2 divides x `2 ;
then A8: x `2 divides ((z `1 ) * (y `2 )) * (x `2 ) by GCD_1:7;
x `2 divides x `2 ;
then A9: x `2 divides ((z `2 ) * (y `1 )) * (x `2 ) by GCD_1:7;
assume z in QClass. t ; :: thesis: z in QClass. y
then (z `1 ) * (t `2 ) = (z `2 ) * (t `1 ) by Def4;
then A10: (z `1 ) * ((x `2 ) * (y `2 )) = (z `2 ) * (t `1 ) by MCART_1:def 2;
A11: ((z `1 ) * (y `2 )) * (x `2 ) = (z `1 ) * ((x `2 ) * (y `2 )) by GROUP_1:def 4
.= (z `2 ) * (((y `1 ) * (x `2 )) + ((0. I) * (y `2 ))) by A4, A10, MCART_1:def 1
.= (z `2 ) * (((y `1 ) * (x `2 )) + (0. I)) by VECTSP_1:39
.= (z `2 ) * ((y `1 ) * (x `2 )) by RLVECT_1:10
.= ((z `2 ) * (y `1 )) * (x `2 ) by GROUP_1:def 4 ;
(z `1 ) * (y `2 ) = ((z `1 ) * (y `2 )) * (1_ I) by VECTSP_1:def 13
.= ((z `1 ) * (y `2 )) * ((x `2 ) / (x `2 )) by A3, GCD_1:9
.= (((z `2 ) * (y `1 )) * (x `2 )) / (x `2 ) by A3, A11, A8, GCD_1:11
.= ((z `2 ) * (y `1 )) * ((x `2 ) / (x `2 )) by A3, A9, GCD_1:11
.= ((z `2 ) * (y `1 )) * (1_ I) by A3, GCD_1:9
.= (z `2 ) * (y `1 ) by VECTSP_1:def 13 ;
hence z in QClass. y by Def4; :: thesis: verum

end;

( qadd u,(q0. I) = QClass. (padd y,x) & qadd (q0. I),u = QClass. (padd x,y) ) by A1, A2, Th11;
hence ( qadd u,(q0. I) = u & qadd (q0. I),u = u ) by A2, A5, A7, SUBSET_1:8; :: thesis: verum