consider x being Element of Q. I such that
A1: u = QClass. x by Def5;
x `2 <> 0. I by Th2;
then reconsider t = [(- (x `1)),(x `2)] as Element of Q. I by Def1;
set M = QClass. t;
A2: for z being Element of Q. I st ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) holds
z in QClass. t

proof

let z be Element of Q. I; :: thesis: ( ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) implies z in QClass. t )
given a being Element of Q. I such that A3: a in u and
A4: (z `1) * (a `2) = (z `2) * (- (a `1)) ; :: thesis: z in QClass. t
A5: (a `1) * (x `2) = (a `2) * (x `1) by A1, A3, Def4;
A6: ((z `1) * (x `2)) * (a `2) = ((z `2) * (- (a `1))) * (x `2) by A4, GROUP_1:def 3
.= (- ((z `2) * (a `1))) * (x `2) by GCD_1:48
.= ((- (z `2)) * (a `1)) * (x `2) by GCD_1:48
.= (- (z `2)) * ((a `2) * (x `1)) by A5, GROUP_1:def 3
.= ((- (z `2)) * (x `1)) * (a `2) by GROUP_1:def 3
.= (- ((z `2) * (x `1))) * (a `2) by GCD_1:48
.= ((z `2) * (- (x `1))) * (a `2) by GCD_1:48 ;
A7: a `2 <> 0. I by Th2;
a `2 divides a `2 ;
then A8: a `2 divides ((z `2) * (- (x `1))) * (a `2) by GCD_1:7;
a `2 divides a `2 ;
then A9: a `2 divides ((z `1) * (x `2)) * (a `2) by GCD_1:7;
(z `1) * (t `2) = (z `1) * (x `2) by MCART_1:def 2
.= ((z `1) * (x `2)) * (1_ I) by VECTSP_1:def 4
.= ((z `1) * (x `2)) * ((a `2) / (a `2)) by A7, GCD_1:9
.= (((z `2) * (- (x `1))) * (a `2)) / (a `2) by A7, A6, A9, GCD_1:11
.= ((z `2) * (- (x `1))) * ((a `2) / (a `2)) by A7, A8, GCD_1:11
.= ((z `2) * (- (x `1))) * (1_ I) by A7, GCD_1:9
.= (z `2) * (- (x `1)) by VECTSP_1:def 4
.= (z `2) * (t `1) by MCART_1:def 1 ;
hence z in QClass. t by Def4; :: thesis: verum

end;

for z being Element of Q. I st z in QClass. t holds
ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) )

proof

let z be Element of Q. I; :: thesis: ( z in QClass. t implies ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) )
assume z in QClass. t ; :: thesis: ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) )
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then (z `1) * (x `2) = (z `2) * (t `1) by MCART_1:def 2
.= (z `2) * (- (x `1)) by MCART_1:def 1 ;
hence ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) by A1, Th6; :: thesis: verum

end;

hence ex b₁ being Element of Quot. I st
for z being Element of Q. I holds
( z in b₁ iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) by A2; :: thesis: verum