consider y being Element of Q. I such that
A1: v = QClass. y by Def5;
consider x being Element of Q. I such that
A2: u = QClass. x 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 = [((x `1 ) * (y `1 )),((x `2 ) * (y `2 ))] as Element of Q. I by Def1;
set M = QClass. t;
A3: for z being Element of Q. I st z in QClass. t holds
ex a, b being Element of Q. I st
( a in u & b in v & (z `1 ) * ((a `2 ) * (b `2 )) = (z `2 ) * ((a `1 ) * (b `1 )) )

proof

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

end;

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

proof

let z be Element of Q. I; :: thesis: ( ex a, b being Element of Q. I st
( a in u & b in v & (z `1 ) * ((a `2 ) * (b `2 )) = (z `2 ) * ((a `1 ) * (b `1 )) ) implies z in QClass. t )
given a, b being Element of Q. I such that A6: a in u and
A7: b in v and
A8: (z `1 ) * ((a `2 ) * (b `2 )) = (z `2 ) * ((a `1 ) * (b `1 )) ; :: thesis: z in QClass. t
A9: (a `1 ) * (x `2 ) = (a `2 ) * (x `1 ) by A2, A6, Def4;
A10: (b `1 ) * (y `2 ) = (b `2 ) * (y `1 ) by A1, A7, Def4;
( a `2 <> 0. I & b `2 <> 0. I ) by Th2;
then A11: (a `2 ) * (b `2 ) <> 0. I by VECTSP_2:def 5;
A12: (a `2 ) * (b `2 ) divides (z `2 ) * ((a `1 ) * (b `1 )) by A8, GCD_1:def 1;
then A13: (a `2 ) * (b `2 ) divides ((z `2 ) * ((a `1 ) * (b `1 ))) * ((x `2 ) * (y `2 )) by GCD_1:7;
(a `2 ) * (b `2 ) divides (a `2 ) * (b `2 ) ;
then (a `2 ) * (b `2 ) divides ((z `2 ) * ((x `1 ) * (y `1 ))) * ((a `2 ) * (b `2 )) by GCD_1:7;
then A14: (((z `2 ) * ((x `1 ) * (y `1 ))) * ((a `2 ) * (b `2 ))) / ((a `2 ) * (b `2 )) = ((z `2 ) * ((x `1 ) * (y `1 ))) * (((a `2 ) * (b `2 )) / ((a `2 ) * (b `2 ))) by A11, GCD_1:11
.= ((z `2 ) * ((x `1 ) * (y `1 ))) * (1_ I) by A11, GCD_1:9
.= (z `2 ) * ((x `1 ) * (y `1 )) by VECTSP_1:def 13 ;
((z `2 ) * ((a `1 ) * (b `1 ))) / ((a `2 ) * (b `2 )) = z `1 by A8, A12, A11, GCD_1:def 4;
then (z `1 ) * ((x `2 ) * (y `2 )) = (((z `2 ) * ((a `1 ) * (b `1 ))) * ((x `2 ) * (y `2 ))) / ((a `2 ) * (b `2 )) by A12, A11, A13, GCD_1:11
.= ((z `2 ) * (((a `1 ) * (b `1 )) * ((x `2 ) * (y `2 )))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * ((a `1 ) * ((b `1 ) * ((x `2 ) * (y `2 ))))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * ((a `1 ) * ((x `2 ) * ((b `1 ) * (y `2 ))))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * (((a `2 ) * (x `1 )) * ((b `1 ) * (y `2 )))) / ((a `2 ) * (b `2 )) by A9, GROUP_1:def 4
.= ((z `2 ) * ((x `1 ) * ((a `2 ) * ((b `2 ) * (y `1 ))))) / ((a `2 ) * (b `2 )) by A10, GROUP_1:def 4
.= ((z `2 ) * ((x `1 ) * ((y `1 ) * ((a `2 ) * (b `2 ))))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * (((x `1 ) * (y `1 )) * ((a `2 ) * (b `2 )))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= (((z `2 ) * ((x `1 ) * (y `1 ))) * ((a `2 ) * (b `2 ))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4 ;
then (z `1 ) * (t `2 ) = (z `2 ) * ((x `1 ) * (y `1 )) by A14, MCART_1:def 2
.= (z `2 ) * (t `1 ) by MCART_1:def 1 ;
hence z in QClass. t by Def4; :: thesis: verum

end;

QClass. t is Element of Quot. I by Def5;
hence ex b₁ being Element of Quot. I st
for z being Element of Q. I holds
( z in b₁ iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1 ) * ((a `2 ) * (b `2 )) = (z `2 ) * ((a `1 ) * (b `1 )) ) ) by A5, A3; :: thesis: verum