consider x being Element of Q. I such that
A2: u = QClass. x by Def5;
x `1 <> 0. I

proof

assume x `1 = 0. I ; :: thesis: contradiction
then A3: x in q0. I by Def8;
x in u by A2, Th6;
then u meets q0. I by A3, XBOOLE_0:3;
hence contradiction by A1, Th9; :: thesis: verum

end;

then reconsider t = [(x `2),(x `1)] as Element of Q. I by Def1;
set M = QClass. t;
A4: for z being Element of Q. I st ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) 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 `1) = (z `2) * (a `2) ) implies z in QClass. t )
given a being Element of Q. I such that A5: a in u and
A6: (z `1) * (a `1) = (z `2) * (a `2) ; :: thesis: z in QClass. t
A7: (a `1) * (x `2) = (a `2) * (x `1) by A2, A5, Def4;
A8: ((z `1) * (t `2)) * (a `2) = ((z `1) * (x `1)) * (a `2) by MCART_1:def 2
.= (z `1) * ((a `1) * (x `2)) by A7, GROUP_1:def 4
.= ((z `2) * (a `2)) * (x `2) by A6, GROUP_1:def 4
.= ((z `2) * (a `2)) * (t `1) by MCART_1:def 1
.= ((z `2) * (t `1)) * (a `2) by GROUP_1:def 4 ;
A9: a `2 <> 0. I by Th2;
a `2 divides a `2 ;
then A10: a `2 divides ((z `2) * (t `1)) * (a `2) by GCD_1:7;
a `2 divides a `2 ;
then A11: a `2 divides ((z `1) * (t `2)) * (a `2) by GCD_1:7;
(z `1) * (t `2) = ((z `1) * (t `2)) * (1_ I) by VECTSP_1:def 13
.= ((z `1) * (t `2)) * ((a `2) / (a `2)) by A9, GCD_1:9
.= (((z `2) * (t `1)) * (a `2)) / (a `2) by A9, A8, A11, GCD_1:11
.= ((z `2) * (t `1)) * ((a `2) / (a `2)) by A9, A10, GCD_1:11
.= ((z `2) * (t `1)) * (1_ I) by A9, GCD_1:9
.= (z `2) * (t `1) by VECTSP_1:def 13 ;
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 `1) = (z `2) * (a `2) )

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 `1) = (z `2) * (a `2) ) )
assume z in QClass. t ; :: thesis: ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) )
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then (z `1) * (x `1) = (z `2) * (t `1) by MCART_1:def 2
.= (z `2) * (x `2) by MCART_1:def 1 ;
hence ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) by A2, 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 `1) = (z `2) * (a `2) ) ) by A4; :: thesis: verum