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 `2 )) + ((y `1 ) * (x `2 ))),((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 `2 )) + ((b `1 ) * (a `2 ))) )

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 `2 )) + ((b `1 ) * (a `2 ))) ) )
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 `2 )) + ((b `1 ) * (a `2 ))) )
then (z `1 ) * (t `2 ) = (z `2 ) * (t `1 ) by Def4;
then (z `1 ) * (t `2 ) = (z `2 ) * (((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) by MCART_1:def 1;
then A4: (z `1 ) * ((x `2 ) * (y `2 )) = (z `2 ) * (((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) 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 `2 )) + ((b `1 ) * (a `2 ))) ) 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 `2 )) + ((b `1 ) * (a `2 ))) ) 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 `2 )) + ((b `1 ) * (a `2 ))) ) 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 `2 )) + ((b `1 ) * (a `2 ))) ; :: thesis: z in QClass. t
A9: (b `1 ) * (y `2 ) = (b `2 ) * (y `1 ) by A1, A7, Def4;
( a `2 <> 0. I & b `2 <> 0. I ) by Th2;
then A10: (a `2 ) * (b `2 ) <> 0. I by VECTSP_2:def 5;
A11: (a `1 ) * (x `2 ) = (a `2 ) * (x `1 ) by A2, A6, Def4;

now

per cases ( ((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )) = 0. I or ((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )) <> 0. I ) ;

case A12: ((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )) = 0. I ; :: thesis: z in QClass. t

then 0. I = (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) * ((x `2 ) * (y `2 )) by VECTSP_1:39
.= ((((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) * (x `2 )) * (y `2 ) by GROUP_1:def 4
.= ((((a `1 ) * (b `2 )) * (x `2 )) + (((b `1 ) * (a `2 )) * (x `2 ))) * (y `2 ) by VECTSP_1:def 12
.= ((((a `1 ) * (b `2 )) * (x `2 )) * (y `2 )) + ((((b `1 ) * (a `2 )) * (x `2 )) * (y `2 )) by VECTSP_1:def 12
.= ((((a `1 ) * (x `2 )) * (b `2 )) * (y `2 )) + (((x `2 ) * ((a `2 ) * (b `1 ))) * (y `2 )) by GROUP_1:def 4
.= ((((a `1 ) * (x `2 )) * (b `2 )) * (y `2 )) + ((x `2 ) * (((a `2 ) * (b `1 )) * (y `2 ))) by GROUP_1:def 4
.= ((((a `2 ) * (x `1 )) * (b `2 )) * (y `2 )) + ((x `2 ) * ((a `2 ) * ((b `1 ) * (y `2 )))) by A11, GROUP_1:def 4
.= ((((a `2 ) * (x `1 )) * (b `2 )) * (y `2 )) + ((x `2 ) * (((a `2 ) * (b `2 )) * (y `1 ))) by A9, GROUP_1:def 4
.= ((((a `2 ) * (x `1 )) * (b `2 )) * (y `2 )) + (((x `2 ) * (y `1 )) * ((a `2 ) * (b `2 ))) by GROUP_1:def 4
.= ((y `2 ) * ((x `1 ) * ((a `2 ) * (b `2 )))) + (((x `2 ) * (y `1 )) * ((a `2 ) * (b `2 ))) by GROUP_1:def 4
.= (((y `2 ) * (x `1 )) * ((a `2 ) * (b `2 ))) + (((x `2 ) * (y `1 )) * ((a `2 ) * (b `2 ))) by GROUP_1:def 4
.= (((y `2 ) * (x `1 )) + ((x `2 ) * (y `1 ))) * ((a `2 ) * (b `2 )) by VECTSP_1:def 12 ;
then A13: ((y `2 ) * (x `1 )) + ((x `2 ) * (y `1 )) = 0. I by A10, VECTSP_2:def 5;
(z `2 ) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) = 0. I by A12, VECTSP_1:39;
then z `1 = 0. I by A8, A10, VECTSP_2:def 5;
then (z `1 ) * (t `2 ) = 0. I by VECTSP_1:39
.= (z `2 ) * (((y `2 ) * (x `1 )) + ((x `2 ) * (y `1 ))) by A13, VECTSP_1:39
.= (z `2 ) * (t `1 ) by MCART_1:def 1 ;
hence z in QClass. t by Def4; :: thesis: verum

end;

case A14: ((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )) <> 0. I ; :: thesis: z in QClass. t

((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )) divides ((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )) ;
then A15: ((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )) divides ((z `1 ) * ((y `2 ) * (x `2 ))) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GCD_1:7;
A16: ((z `1 ) * (((y `2 ) * (x `2 )) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) = (((z `1 ) * ((y `2 ) * (x `2 ))) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * ((y `2 ) * (x `2 ))) * ((((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )))) by A14, A15, GCD_1:11
.= ((z `1 ) * ((y `2 ) * (x `2 ))) * (1_ I) by A14, GCD_1:9
.= (z `1 ) * ((x `2 ) * (y `2 )) by VECTSP_1:def 13 ;
A17: ((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )) divides (z `1 ) * ((a `2 ) * (b `2 )) by A8, GCD_1:def 1;
then A18: ((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )) divides ((z `1 ) * ((a `2 ) * (b `2 ))) * (((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) by GCD_1:7;
((z `1 ) * ((a `2 ) * (b `2 ))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) = z `2 by A8, A14, A17, GCD_1:def 4;
then (z `2 ) * (((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) = (((z `1 ) * ((a `2 ) * (b `2 ))) * (((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 )))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by A14, A17, A18, GCD_1:11
.= ((((z `1 ) * (a `2 )) * (b `2 )) * (((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 )))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= (((z `1 ) * (a `2 )) * ((b `2 ) * (((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * ((a `2 ) * ((b `2 ) * (((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 )))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * ((a `2 ) * (((b `2 ) * ((x `1 ) * (y `2 ))) + ((b `2 ) * ((y `1 ) * (x `2 )))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by VECTSP_1:def 11
.= ((z `1 ) * (((a `2 ) * ((b `2 ) * ((x `1 ) * (y `2 )))) + ((a `2 ) * ((b `2 ) * ((y `1 ) * (x `2 )))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by VECTSP_1:def 11
.= ((z `1 ) * (((a `2 ) * (((b `2 ) * (x `1 )) * (y `2 ))) + ((a `2 ) * ((b `2 ) * ((y `1 ) * (x `2 )))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * ((((a `2 ) * ((x `1 ) * (b `2 ))) * (y `2 )) + ((a `2 ) * ((b `2 ) * ((y `1 ) * (x `2 )))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * (((((a `1 ) * (x `2 )) * (b `2 )) * (y `2 )) + ((a `2 ) * ((b `2 ) * ((y `1 ) * (x `2 )))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by A11, GROUP_1:def 4
.= ((z `1 ) * (((((a `1 ) * (x `2 )) * (b `2 )) * (y `2 )) + ((a `2 ) * (((b `1 ) * (y `2 )) * (x `2 ))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by A9, GROUP_1:def 4
.= ((z `1 ) * (((y `2 ) * ((x `2 ) * ((a `1 ) * (b `2 )))) + ((a `2 ) * (((b `1 ) * (y `2 )) * (x `2 ))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * (((y `2 ) * ((x `2 ) * ((a `1 ) * (b `2 )))) + ((x `2 ) * ((a `2 ) * ((b `1 ) * (y `2 )))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * (((y `2 ) * ((x `2 ) * ((a `1 ) * (b `2 )))) + ((x `2 ) * ((y `2 ) * ((b `1 ) * (a `2 )))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * ((((y `2 ) * (x `2 )) * ((a `1 ) * (b `2 ))) + ((x `2 ) * ((y `2 ) * ((b `1 ) * (a `2 )))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * ((((y `2 ) * (x `2 )) * ((a `1 ) * (b `2 ))) + (((y `2 ) * (x `2 )) * ((b `1 ) * (a `2 ))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `1 ) * (((y `2 ) * (x `2 )) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))))) / (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by VECTSP_1:def 11 ;
then (z `1 ) * (t `2 ) = (z `2 ) * (((y `2 ) * (x `1 )) + ((x `2 ) * (y `1 ))) by A16, MCART_1:def 2
.= (z `2 ) * (t `1 ) by MCART_1:def 1 ;
hence z in QClass. t by Def4; :: thesis: verum

end;

end;

end;

hence z in QClass. t ; :: 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 `2 )) + ((b `1 ) * (a `2 ))) ) ) by A5, A3; :: thesis: verum