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 4
.= (- ((z `2 ) * (a `1 ))) * (x `2 ) by GCD_1:51
.= ((- (z `2 )) * (a `1 )) * (x `2 ) by GCD_1:51
.= (- (z `2 )) * ((a `2 ) * (x `1 )) by A5, GROUP_1:def 4
.= ((- (z `2 )) * (x `1 )) * (a `2 ) by GROUP_1:def 4
.= (- ((z `2 ) * (x `1 ))) * (a `2 ) by GCD_1:51
.= ((z `2 ) * (- (x `1 ))) * (a `2 ) by GCD_1:51 ;
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 13
.= ((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 13
.= (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